From Natural-Language Propositions to Lean Proofs: Proof-Search Feedback for Source-Grounded Re-Formalization

End-to-end formalization and proving transforms a natural-language mathematical proposition into a Lean theorem together with a kernel-checked proof. In the proposition-only setting, no proof is supplied, so the system must discover the proof itself. Once a formalization is accepted, however, many pipelines keep it fixed during proof search, leaving proof failures unable to expose semantic defects in the statement. We call the resulting rate of self-accepted but unproved formalizations the operational semantic–proof closure gap. We study whether concrete proof-failure information produced by a model can help that same model discover such defects. We instantiate a verify-before-revise loop at the proposition-only Lean formalization–proof boundary: when proof search produces a suspected-false signal, a separate semantic audit compares the root formalization with the original proposition, and a revision is allowed only when the audit identifies a concrete, proposition-grounded discrepancy. Across two models and two datasets, the closed loop reduces the closure gap and improves externally validated end-to-end success, including BEq-validated success.