Partial Soundness: Natural Language Theorem Proving with Machine-Checked Logical Structure

Large language models are increasingly proficient in mathematical reasoning tasks in natural language, but such outputs can lack formal guarantees, whereas fully formal theorem proving remains difficult due to various factors. We introduce Partial Soundness, a theorem-proving framework that bridges these settings through machine-checked proof structure. Given a theorem, the framework decomposes it into intermediate subgoals, formalizes the subgoals in Lean, and verifies that they are sufficient to derive the target theorem before any natural language proof is generated. Natural language proofs are then produced and assembled into a complete proof. This yields a partial soundness guarantee: while leaf-level reasoning remains informal, the logical dependency structure of the proof is formally verified. We also introduce INFormalRA, a dataset of 114 undergraduate real analysis theorems paired with Lean formalizations. Experiments on INFormalRA and existing benchmarks demonstrate that the proposed framework produces proofs with machine-checked logical structure and more interpretable intermediate reasoning while displaying reasonable proof-generation performance. These results suggest that Partial Soundness provides a practical middle ground between unconstrained natural language theorem proving and fully formal proof generation.