Formalizing and machine-checking mathematics

Claims

• observationsingle paper↑1↓0
  On 1,000 Lean 4 targets from computational and applied mathematics textbooks (optimization, numerical linear algebra, numerical analysis), whose statements depend on locally introduced definitions, current provers solve about 62-72% of a 200-problem sample, so applied-math formalization is tractable but not saturated and requires recovering textbook context to state problems faithfully.
• observationsingle paper↑1↓0
  On 450 Lean 4 theorem targets in graduate stochastic processes — a field thinly covered by Mathlib — a tool-using frontier agent (Opus 4.8 with Lean LSP access, one 15-minute run per problem) proves only 34.9%, and the rate varies widely by topic, from about 5% on renewal processes to about 62% on martingales and stopping.
• observationsingle paper↑1↓0
  On 613 research-level theorems from six real Lean Blueprint formalization projects, the best current prover reaches only about a 10% pass rate, so progress on curated benchmarks such as miniF2F does not carry over to theorems embedded in live formalization projects with their own definitions and lemmas.
• observationsingle paper↑1↓0
  Autoformalization of problem statements into Lean 4 improves sharply when the formalizer can call the Lean compiler for syntax and a multi-model judge panel for meaning and revise on the feedback: a 32B model's consistency Pass@1 on CombiBench rose from about 24% without tools to about 65% with them, and an 8B distilled version reached about 91% on FormalMath-Lite, with the judge ensemble holding false-positive consistency below 6%.
• observationsingle paper↑1↓0
  A Lean prover trained with large-scale agentic reinforcement learning against the Lean checker, paired with a test-time workflow that drafts in natural language before formalizing, solved 88% of PutnamBench (undergraduate), 80% of Fate-H (graduate) and 33% of Fate-X (PhD-level), and 11 of 12 Putnam 2025 problems, at a smaller compute budget than prior systems, so formal proving at undergraduate level is largely solved while PhD-level remains open.

Techniques

• Natural-language draft, then formalize, with checker-in-the-training
  Have the model write an informal proof sketch first, translate it into Lean, and refine against compiler feedback; train the prover by reinforcement learning on long interactions with Lean so it accumulates experience of what checks.
• Tool-feedback autoformalization with compiler and judge paneprocess
  Let the formalizer emit a Lean statement, compile it, and ask a panel of models whether it matches the informal statement; feed both results back and let the model revise, training it on such tool-calling traces so revisions become effectiv

Sources

Every paper, post or observation behind this capability. Ones cited by a claim show the claim and its stance; ones filed directly are about the capability but have no claim drafted from them yet. Open one to add support or contest it.

• StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean2026-09-08
  ↑ supports a claim here
• CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean2026-05-17
  ↑ supports a claim here
• Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience2025-12-19
  ↑ supports a claim here
• RLMEval: Evaluating Research-Level Neural Theorem Proving2025-10-29
  ↑ supports a claim here
• Autoformalizer with Tool Feedback2025-10-08
  ↑ supports a claim here