Mathesis translates an informal problem into a Lean 4 statement, scores candidate formalizations for syntactic and semantic quality, and uses downstream prover feedback to prefer statements that can support machine-checked proofs.
The Mathesis paper introduced an autoformalization-and-proving pipeline trained with reinforcement and preference feedback, together with LeanScorer and the Gaokao-Formal benchmark, and reported that pairing its autoformalizer with existing provers substantially improved end-to-end proving accuracy on natural-language problems.
Mathesis translates an informal problem into a Lean 4 statement, scores candidate formalizations for syntactic and semantic quality, and uses downstream prover feedback to prefer statements that can support machine-checked proofs. Gaokao-Formal provides hundreds of challenging proof problems derived from Chinese college-entrance examinations for evaluating this full pipeline.
The work moved formal-math systems closer to the way mathematical problems are actually presented to humans: in natural language. It also made autoformalization quality part of an end-to-end proving objective rather than an isolated translation task.
Significance rationale: Mathesis addressed a major interface bottleneck in neural theorem proving by coupling learned autoformalization of ordinary mathematical language with downstream Lean proof generation and feedback, rather than assuming an expert-written formal statement as the starting point.
The arXiv research record introduced Mathesis, LeanScorer and Gaokao-Formal and reported end-to-end formal-proving results.
The public Mathesis repository exposes implementation and project resources, and the work later appeared at ICLR 2026. Machine-checked refers to Lean acceptance within the evaluated proof pipeline; it does not imply independent replay of every experiment or semantic equivalence judgment.
No corrections recorded.
