Long-Horizon Formalization Crosses into Research-Level Mathematics: Fermat's Last Theorem, MIP*=RE, and Ramsey
Highlights of This Issue
The main thread of this issue is the transition of long-horizon automated formalization from proving individual theorems to formalizing entire research papers and even entire research fields. Three milestone-level artifacts appear simultaneously: Anthropic used the Prove2Me platform to complete a fully machine-verified proof of Fermat's Last Theorem in 11 days (13 million lines of Lean, 29,500 intermediate theorems, relying only on Lean's three standard axioms, independently rechecked by comparator and nanoda); FormalFlow took 63 days to formalize the core theorem of MIP*=RE (quantum soundness of the classical low-individual-degree test, 126,367 lines without sorry); Trellis used a deterministic process kernel to end-to-end formalize two recent Ramsey papers. Last issue we were still discussing the robustness of evaluation; this issue, proof search has advanced to research-level mathematics, measured in "papers."
These three share a trend: treating "proof composition" and "statement drift" as first-class citizens to be explicitly governed, rather than left to agent free play. FormalFlow's proof-gap protocol distinguishes paper corrections from formalization fixes and hardens failure modes found in review into automated CI checks; Trellis operationalizes "rigor" as machine-checkable monotonic refinement, making progress a checkable property of tablet state; Prove2Me uses DAG-ified theorem statements with natural language descriptions to support cross-agent parallelism. This aligns with the vision from Issue 4 when the Prove2Me platform was released—this issue it truly ran through Fermat's Last Theorem.
The discovery side is also moving from "solving given problems" to "choosing which problems are worth proving." Learning to Discover Interesting Mathematics gives the first computable, library-grounded definition of "intrinsic interestingness" and proves its strong correlation with downstream utility, advancing conjecture generation from random sampling to an optimizable objective; ProofGap shifts evaluation granularity from complete theorems down to step-level local obligations. On the training side, Direct Optimization of Generators for the first time explicitly aligns search strategy structure with training objectives.
Community and Developments
- Formalization of Fermat's Last Theorem completed: Anthropic released a fully machine-verified proof of Fermat's Last Theorem, 13 million lines of Lean, 29,500 intermediate theorems, relying only on Lean's three standard axioms, independently rechecked by comparator and nanoda; the official announcement details how the Prove2Me platform uses DAG-ified theorem statements to support multi-agent parallelism. This is the most direct payoff since the Prove2Me platform release in Issue 4.
- Independent kernel verification becoming default: The Lean 4 core bundles the independent lean4lean external checker into the release toolchain; combined with FLT's comparator/nanoda dual rechecking, independent verification is moving from research prototype to standard artifact.
- Community benchmarks and competitions: Terence Tao, together with Lean core developers, launched the SAIR Lean Kernel Challenge, focusing on kernel verification computation speed as a new evaluation axis; Mathlib added the
basifytactic to translate ENNReal/ENat/PNat goals to Nat/Real, improving automation for extended arithmetic. - Courses and trust signals: The Fields Institute is offering a graduate course on mathematical formalization and automated formalization; the Lean reference manual now classifies unreviewed AI proofs as malicious code, reflecting the community's adjusted trust posture toward AI-batch-produced proofs.
- IMO 2026 ecosystem: Multiple open-source pipelines claim complete solutions to IMO 2026, including Pramaana Labs (Panini automated formalization + Hardy proof search), Boundless Intuition's Dirac, and deedy's seven-model comparison audit; others note that formal verification and competition judging are different things, and benchmark saturation is blurring this distinction.
Open Questions
- FormalFlow's 25 gap notes corrected errors in published theorem statements and error budgets—when AI formalization becomes the norm, "errors in paper statements" will be exposed by machine verification. Can the "number and type of gap notes" be standardized as a mandatory reporting metric for long-horizon formalization projects, allowing downstream comparison of governance quality across systems?
- Trellis operationalizes rigor as "any step can be routinely refined," while FormalFlow uses the proof-gap protocol to govern statement drift—can these two definitions of "progress" be unified into a single checkable monotonicity condition, serving as a universal invariant for agentic formalization?
- The interestingness metric turns "what is worth proving" from human taste into an optimizable objective, but will its definition (proof length/statement length) degrade in a self-extending library—as the library grows and premises multiply, conditional proof difficulty changes; is the interestingness ranking stable?
- The "silent regression" and "sycophancy" failure modes from last issue have received engineering responses in Trellis's three verification channels (substantive/correspondence/reliability) and FormalFlow's CI-hardened mechanisms—but these are all inference-time governance. Can such failures be used as training signals, combined with Issue 4's Process-Verified RL, so that models learn fidelity rather than regression during training?
Papers in this issue
FormalFlow, a human-supervised multi-agent framework, machine-checked the quantum soundness of LIDT in Lean 4 within 63 days, uncovering 5 errors in the published proof.
Editor's noteFormalFlow completed a 126,367-line Lean 4 formalization of the core theorem of MIP*=RE (quantum soundness of the classical low-individual-degree test) in 63 days, with no sorry and using only standard axioms. Compared to Issue 2's LeanMarathon and Goedel-Architect, its increment lies in explicit governance of "statement drift" and "proof composition": shared blueprint, nested feedback loops, a proof-gap protocol distinguishing paper corrections from formalization fixes, and hardening failure modes found in review into automated CI checks. The 25 gap notes corrected errors in published theorem statements and error budgets; the public repository, blueprint, and development history make it a reproducible artifact.
Trellis autoformalized two recent Ramsey theory breakthroughs into complete Lean proofs using generalist LLM agents, enforcing incremental progress through a deterministic process kernel rather than task-specific training.
Editor's noteTrellis uses a deterministic process kernel (35k lines of Rust + TLA+ specification) to operationalize "rigor" as machine-checkable monotonic refinement: three verification channels (substantive, correspondence, reliability) plus fingerprint reopening, with human-approved semantic closure making faithfulness independent of agent reliability. Compared to LEAP, Goedel-Architect, and Magenta, which rely on LLM judgment or training, Trellis makes "progress" a checkable property of tablet state, using off-the-shelf models to end-to-end formalize two recent Ramsey papers (including work breaking a 50-year exponential barrier), with complete cycle checkpoints public.
A quantitative metric of mathematical interestingness, defined as proof difficulty divided by statement length, enables LLMs to autonomously discover novel, useful theorems beyond existing mathematical libraries.
Editor's noteGives the first computable, library-grounded definition of "intrinsic interestingness"—the ratio of proof length to statement description length—and proves its strong correlation with downstream utility (Spearman 0.756). Trains a 27B model to predict conditional proof difficulty, outperforming frontier general-purpose models; using interestingness as a reward to guide conjecture models reduces overlap of generated theorems with Mathlib from 91.9% to 30.6%, providing a discovery signal for self-extending formalization libraries without human targets. Compared to Stellar Colosseum's multi-agent orchestration, its increment is an optimizable quantitative objective.
Compute-aligned training losses that reweight per-tactic cross-entropy gradients consistently outperform standard cross-entropy across all six search strategies in Lean theorem proving, with gains scaling as test-time compute grows.
Editor's noteExtends Compute-Aligned Training from flat search (Pass@N) to branching tree search (BFS/DFS/MCTS), deriving per-tactic gradient weights via trace-supported surrogate objectives and introducing a search-agnostic uniform-allocation loss. Compared to Issue 4's Process-Verified RL and Issue 2's OProver, it is the first to systematically model the alignment between search strategy structure and training objectives, theoretically characterizing the impact of off-trace behavior (bypass/trap channels) on weights. Validated on Lean benchmarks across six search strategies, with code public.
ProofGap decomposes 26,116 step-level proof gaps from Demidovich exercises, showing local obligations are far more tractable (35% Pass@8) than complete theorems (4%), with general-purpose models now outperforming specialized provers.
Editor's noteA step-level benchmark that decomposes local proof obligations from natural language textbook solutions: for 3015 problems from Demidovich's "Problems in Mathematical Analysis," it produces 26,116 gaps, each aligned with specific steps in the source solution, supporting fine-grained diagnosis of local formal reasoning. Compared to miniF2F/ProofNet, which evaluate complete theorems, and FormalML, which extracts subgoals from existing formalizations, its construction pipeline (Relaxed NFL→Core NFL→proof-gap generation) is a new methodology for creating step-level benchmarks at scale; the Lean version and ground-truth proofs are public.
Lean Pool is a living, AI-maintained archive of 211 formalized Lean projects with 837 main results, kept compatible across six dependency upgrades.
Editor's noteA living archive of formalized mathematics grown, maintained, and optimized by AI agents, positioned as a formalized arXiv. Compared to Tau Ceti (integrated into a shared API) and the Palomar Registry (registering verified versions of independent repositories), its increment lies in explicitly merging independently developed, attributed projects into a single maintenance environment, with agent-driven dependency upgrades, library-level proof shortening, and compilation optimization, while recording the operational history of these maintenance processes. Currently contains 211 merged projects and 3.22 million lines of Lean, directly addressing the reuse and maintenance bottleneck for research-level mathematics beyond Mathlib.
Iris-Lean fully reimplements Iris in Lean, outperforming Iris-Rocq in automation speed, and enabling probabilistic program verification via Mathlib integration.
Editor's noteIris-Lean is the first work to fully reimplement the Iris separation logic framework in Lean 4, covering all non-experimental features of Iris-Rocq. Its core increment is replacing setoid equivalence with quotient types and Leibniz equality systems, making rw/simp directly usable and integrating with Mathlib, while using Lean metaprogramming to implement new IPM proof patterns and custom typeclass synthesizers. Leveraging Mathlib's measure theory, it demonstrates continuous-probability program logic (CTE) previously impossible in Rocq, making substantial engineering contributions to the Lean ecosystem and program verification.
