Issue 2: From "Can Prove" to "Trustworthy" — The Governance Layer and Bottleneck Quantification of AI Formal Mathematics
Highlights
The most important signal this issue: the formal mathematics community is shifting from "can prove" to "trustworthy." Terence Tao's announced Palomar registry establishes a community-level admission standard for AI-generated Lean formalizations—using the Lean Comparator to mechanically verify that "the proof proves exactly the stated proposition," an LLM to check semantic alignment of informal statements, and a formalization.yaml metadata standard. It does not claim to be peer review, but rather provides an indexable, auditable "preprint server"-style record layer for the flood of AI proofs, directly addressing the "trust chain for AI-generated proofs" question raised in the previous issue.
Alongside the governance layer, a landmark case of the new workflow "AI proofs digested by human experts" has emerged: Tao digested Mazur's AI-assisted proof of the Sendov conjecture into a ~15,000-line streamlined Lean formalization, a significant reduction from the original 90,000+ lines, and for the first time formalized the Phelps–Rodriguez form (including equality classification). This marks the first high-profile case in the Lean 4 ecosystem of "human digestion of machine-generated proofs into library-grade artifacts." Meanwhile, the AlphaProof Nexus audit points out that at least 4 of the 9 "open" Erdős problems it claims to solve were already solved in human literature, and 1 is only a partial result—reminding us that claims of "open problems" themselves need auditing.
At the methodological level, several works this issue quantify and make actionable the judgment that "automatic formalization is a sharper bottleneck than theorem proving." FormalTCS is the first to decompose the research pipeline on an end-to-end benchmark targeting frontier TCS research, measuring automatic formalization (NC2FT max 11.5) far below proving given formal statements (FT2FP max 28.6), and finding that "research taste" is another major obstacle to autonomous research. This aligns with the community's ongoing concern that "compilation success ≠ semantic fidelity."
Community and Dynamics
- Palomar registry opens: The Palomar registry, incubated by Lean FRO and ICARM, opened for submissions this week, with a scientific advisory board including Avigad, Tao, Venkatesh, and others. It uses the Comparator to mechanically verify the correspondence between proof and statement, an LLM to check semantic alignment, and introduces the formalization.yaml metadata standard; Tao has already submitted his Sendov formalization as a test.
- Sendov conjecture digestion and re-formalization: Tao's streamlined formalization is the second Lean formalization of Mazur's AI proof, mathematically a streamlined descendant of the former, but for the first time covering the Phelps–Rodriguez equality classification; the making-of documents a four-day collaborative dialogue with Claude Code, a valuable first-hand resource for studying "human-AI collaborative formalization."
- AlphaProof Nexus's open problem claims audited: The audit report cross-references Tao's AI contributions wiki, pointing out that at least 4 of the 9 claimed Erdős problems were already solved in human literature (e.g., #12 solved by Erdős–Sárközy in 1970), and 1 is only a partial result, with the root cause being the outdated ErdosProblems.com database. This sounds an alarm for verification standards of "open problem" claims.
- Annals Challenge and library building: AnnalsChallenge provides 50 main-theorem-level statements from the Annals of Mathematics (proofs left as sorry), accompanied by many new Mathlib definitions—continuing the judgment that "formalization library building is a bottleneck."
- Lea and Axiom Math engineering progress: Lea is an open-source Lean 4 agent under DARPA's expMath program, enabling "in-place automatic formalization within LaTeX documents" via an Overleaf extension, lowering the barrier for mathematicians; Axiom Math formalizes the polymath "246" prime gap theorem into a reusable PrimeGapsLib. Both require verification of their automation level against actual artifacts.
- Community verification of AI counterexamples: Erdos90 provides a Lean formal verification of OpenAI's Erdős unit-distance counterexample, another instance of community-driven verification of AI mathematics.
Open Questions
- The AlphaProof audit shows that "open problem" claims may be distorted by database lag: what standards should the community establish to determine whether an AI-claimed open problem is indeed open? Can Palomar's mechanical verification be extended (or should it) to the non-mechanical dimension of "novelty"?
- Palomar's statement semantic alignment relies on LLM judgment, which is non-deterministic: how can semantic equivalence certification methods like the bidirectional provability fingerprint proposed in the previous issue be integrated into the registry, making "statement matching" a reproducible mechanical check?
- FormalTCS measures automatic formalization (NC2FT 11.5) far below proving given statements (FT2FP 28.6): is this bottleneck a data/representation issue, or a fundamental limitation of model capability? Can dependency-aware formalization (e.g., MathAtlas's dependency graph) substantially break through it?
- The "agent durability" revealed by LeanMarathon—coherence loss and irreversible errors during long-horizon runs—is there a general fault-tolerant architecture (e.g., frozen edit zones, CI gating) that can be generalized to all agentic formalization systems?
Papers in this issue
LEAP lets general LLMs beat specialized provers in formal math by combining informal blueprint sketches with iterative Lean verification, solving all 12 Putnam 2025 problems.
Editor's noteLEAP's increment lies in combining AND-OR DAG hierarchical memory with interleaved informal-formal planning, enabling a general LLM without specialized fine-tuning to achieve 100% solve rate on Putnam 2025, and on Lean-IMO-Bench improving a general model from <10% to 70%, surpassing the gold-medal-level specialized system Aristotle's 48%. The DAG structure supports lemma reuse and anticipatory lemma planning, mitigating the exponential complexity of Hilbert-style tree search; ablations clearly isolate the contribution of DAG memorization, and code and data are public, making it a must-read for agentic proof search architectures.
FORMALTCS reveals LLMs' autoformalization is the critical bottleneck in frontier TCS research, with top models scoring only 11.5 versus 28.6 on proving human-provided formal statements.
Editor's noteFormalTCS is the first end-to-end benchmark targeting frontier TCS research (STOC/FOCS/SODA/COLT 2025-2026), decomposing the research pipeline into four stages and diagnosing bottlenecks at each stage. The key increment is the first quantification that "automatic formalization (NC2FT max 11.5) is a sharper bottleneck than theorem proving (FT2FP max 28.6)", and finding that "research taste" is another major obstacle to end-to-end autonomous research (only 6 of 64 generated claims passed expert evaluation); 175 expert-verified instances and open-source code make it a complementary benchmark close to real research scenarios.
OProver unifies retrieval, compiler feedback, and iterative repair into a learned policy, achieving state-of-the-art Pass@32 on MiniF2F (93.3%), ProverBench, and PutnamBench with a 32B model.
Editor's noteOProver unifies retrieval, compiler feedback, and iterative repair into a single learnable policy, trained end-to-end via CPT+SFT+RL, with a co-evolution loop that feeds back proven proofs and repair trajectories into the corpus. The core increment is train–inference matching: the same state representation is used across rollout, SFT, and RL, making feedback-conditioned refinement a learned policy rather than a test-time heuristic; the OProofs corpus (with trajectory-level supervision including failed attempts, feedback, and repairs) and ablations are reproducible, achieving 93.3% Pass@32 on MiniF2F.
GOEDEL-ARCHITECT, an open-weight Lean 4 framework using global blueprint refinement, achieves 99.2% pass@1 on MiniF2F and 75.6% on PutnamBench at 555x lower cost than prior pipelines.
Editor's noteGoedel-Architect centers on a global dependency graph blueprint, performing formalization via iterative refinement, using global blueprint rewriting instead of recursive decomposition, allowing parallel proof attempts to share context, and treating negated sub-lemmas and abandoned proofs as structured diagnostic signals. It achieves SOTA on open-weight models at 500x lower cost than comparable open-source pipelines, serving as a reference for building efficient, scalable proof search pipelines.
LeanMarathon's evolving-blueprint harness with contract-scoped agents formalized all seven theorems across four Erdős problems in Lean 4, where a commercial baseline failed.
Editor's noteLeanMarathon targets long-horizon research-level automatic formalization, using a blueprint that simultaneously serves as a formal skeleton, informal proof graph, and record system, paired with contract-scoped agents, CI-gated verification, and frozen edit zones for fault tolerance. Its characterization of "agent durability" failure modes (coherence loss, self-evaluation bias, irreversibility), and the controlled ablation showing "source-blind Refiner + budgeted Worker stopping rule leading to 12-day stagnation," provide actionable design insights not present in prior work.
LLMs excel at closing proof goals but remain weak at choosing definitions and designing APIs, so autoformalization evaluation must shift from compilation success to expert review of library quality.
Editor's noteThis paper is the first to treat expert review itself as the object of study in semi-autonomous formalization, isolating the gap between "kernel acceptance" and "reusable library contribution." Only 1 of 62 definitions was done correctly, showing that agents can fix local mechanical issues but fail at global design decisions (definitions, APIs, theorem generality); the full expert review logs are released as a dataset, providing an actionable standard for evaluation beyond benchmark scores.
MathAtlas, a benchmark of 52k graduate-level theorems and definitions with dependency graphs, shows current autoformalization systems achieve at most 9.8% correctness.
Editor's noteMathAtlas is the first large-scale (~52k entities, ~178k dependencies) graduate-level automatic formalization benchmark, covering 103 textbooks and 87 domains, and the first to introduce an entity-level dependency graph to support dependency-aware evaluation. On the MA-Hard subset, the strongest baseline achieves only 2.6% accuracy, and MA-Align shows that existing metrics degrade on graduate-level mathematics, leaving substantial room for dependency-aware formalization systems; it is a key resource for evaluating such systems.
Pistis achieves faithful formalization of Euclid's proofs by enforcing five checkable conditions, beating prior work 2.89x in human preference and finding genuine citation errors.
Editor's notePistis elevates "fidelity" from an evaluation metric to a first-class constraint in search: via five necessary conditions and the OrderDecompose divide-and-conquer strategy, it tracks reference dependencies, blocks unfaithful shortcuts, and pairs with counterexample search to expose gaps in natural-language proofs. This is a substantial increment over the previous issue's (#1) Beyond Compilation—which measured fidelity gaps but did not enforce them in search; however, code availability is yet to be confirmed, and it is recommended to evaluate with ablation details.
