LLM-based theorem proving systems suffer from hallucinated logical steps and unverifiable reasoning. Current approaches lack mechanisms to detect and correct errors in generated proofs before final output.

ProofNet++ is a neuro-symbolic framework combining a transformer-based LLM (fine-tuned on proof corpora) with symbolic proof tree supervision, a reinforcement learning loop using formal verifiers as reward functions, and an iterative self-correction module. The symbolic reasoning interface bridges autoregressive LLM outputs and formal proof states. The system targets Lean, Isabelle/HOL, and HOL Light environments.

On miniF2F, ProofNet++ achieves 68.4% Formal Proof Success Rate (FPSR) and 81.2% Proof Path Correctness (PPC) with average error distance of 3.2 steps. On mathlib-extract, it reaches 74.9% FPSR and 88.0% PPC. On HOL Light, it achieves 63.5% FPSR and 76.5% PPC.