Architectural Shift in Proof Search: From Local Repair to Global Coordination
Highlights of This Issue
The main theme of this issue is the architectural shift in agentic proof search: from "models writing proofs token by token" to "models only planning/coordinating, with execution delegated to tools and kernels." Two directions are maturing simultaneously. Maestro: Agentic Formal Proof Development by Coordination advances failure handling from "local repair" to "global coordination"—workers return structured diagnostics (routes attempted, auxiliary facts needed, suspected counterexamples), and the coordinator, seeing the entire proof forest, chooses to retry, add lemmas, retract subtrees for replanning, or refute goals, achieving 34/48 on arXivLean, surpassing the native agent's 19/48. SCOPE: Certified Theorem Proving with a Language Model as the Policy Planner is more radical: the model never touches proof text or numbers, only making policy plans within a vocabulary of 194 operators, with a symbolic execution engine handling arithmetic and a compiler rendering Lean text, reaching an 87.6% kernel verification pass rate with a 135M backbone, and providing a theoretical explanation via the "error product law."
The evaluation landscape is also expanding toward "open problems" and "cross-system" dimensions. reuF2F is the first to systematically collect 244 open conjectures from REU undergraduate research projects, formalized in Lean 4, using a bidirectional prove/disprove protocol and dual kernel verification with Comparator+nanoda; ITPEval is the first cross-system formal translation benchmark spanning Lean 4, Rocq, Isabelle, and HOL Light, whose BEq check demonstrates that "type-checking passes" significantly overestimates semantic fidelity. Meanwhile, Structure-Aware Equivalence for Evaluating Autoformalized Statements proposes a role-preserving equivalence relation between syntactic equivalence and full logical equivalence, capable of rejecting pairs that are logically equivalent but mathematically role-irrelevant—directly responding to last issue's assessment that "statement-level formalization is saturating."
Community and Updates
- AlphaProof Nexus releases mechanical formal proof artifacts for the first time: AlphaProof Nexus Results makes public the Lean proof files and accompanying natural language proofs for open problems solved by the system, covering Erdős problems, OEIS, Stacks Project, and AICollaborator deployments, making AlphaProof-class results—previously only announced—reproducible and independently verifiable for the first time.
- Community leaderboard tracks frontier model formalization progress: Lean AI formalization leaderboard records the Lean formalization status of frontier models on major theorems such as the Poincaré conjecture, Friedlander–Iwaniec, and Linnik, serving as status updates rather than methodological contributions.
- Continued questioning of "verification as trust": Verification was never just about certification systematically catalogs failure modes that weaken Lean certificates, including mistranslations, native_decide, kernel bugs, and sorry/axiom; OpenAI Navier-Stokes proof and the Lean critique documents the community debate over the distinction that "kernel checking only verifies the formal statement, not fidelity to the original natural language proof."
- Mathlib 100 theorems list adds external AI proofs: Mathlib changelog records that Feuerbach, the four-color theorem, Fermat's Last Theorem, and others have been given Lean proofs by external AI and added to the 100 theorems list, distinctly marked from internal mathlib efforts.
Open Questions
- Maestro's global coordination relies on frontier closed-source models, and its baseline is a "plain coding agent" rather than the strongest specialized prover—is the benefit of structured failure diagnostics a product of model introspection capabilities, or is the coordination architecture itself transferable to open-weight models and specialized provers?
- SCOPE's "model only plans, does not write text" is effective in constructive discrete mathematics (induction, inequalities, number theory), but can the operator vocabulary be defined in non-constructive fields such as analysis and geometry? Does the error product law hold in these fields as well?
- reuF2F's open problems are drawn from low-attention REU projects to reduce leakage, but the benchmark itself is a static snapshot—as problems are solved and answers diffuse, how can its held-out validity be maintained? Does the ~40% solve ceiling reflect model capability or formalization difficulty?
- Both ITPEval and SAE show that "type-checking passes" overestimates semantic fidelity (BEq passes only 54%)—can structure-aware equivalence scale to become the default verification gate for cross-ITP translation and autoformalization, rather than being demonstrated only on small diagnostic sets?
Papers in this issue
MAESTRO's global coordinator, using structured failure diagnoses, outperforms all published provers on math and code benchmarks, replacing local repair with evidence-driven replanning.
Editor's noteAdvances proof failure handling from "local repair" to "global coordination": workers return structured diagnostics (routes attempted, auxiliary facts needed, suspected counterexamples), and the coordinator, seeing the entire proof forest, chooses to retry, add lemmas, retract subtrees for replanning, or refute goals, and can arbitrarily edit the shared workspace (including discarding proven lemmas). Compared to Issue 10's Lean Graph Search (retrieval-augmented) and Issue 9's LEVER (goal-directed search on AND/OR graphs), the increment lies in explicitly modeling failure causes and allowing global-level replanning; the same framework extends to verified code synthesis (counterexamples sent back to the implementer for repair). Achieves 34/48 on arXivLean, surpassing the native agent's 19/48, with run logs and prompts publicly available. Note the baseline is a plain coding agent rather than the strongest specialized prover, and it relies on frontier closed-source models, but the ablation (naive decomposition) cleanly isolates the contribution of coordination.
SCOPE, using a 135M-parameter model solely as a planner, certifies 87.6% of theorem-proving problems, vastly outperforming 7B direct-generation baselines by separating execution from generation.
Editor's noteProposes a three-part architecture where "the model never touches proof text/numbers, only selects operators": the model does policy planning within a vocabulary of 194 operators, a symbolic execution engine handles arithmetic, and a compiler renders Lean text. Compared to Issue 7's LEAP (goal-directed search on AND/OR graphs, still with the model outputting concrete steps) and Issue 9's LeanPlan (agent generates code+proof, kernel verifies), the increment lies in making "the model does not write proof text" an architectural principle, and a 2×2 factorial experiment proves that "state visibility at decision time" is a first-order determinant of accuracy (53.7%→87.6% after correction), while also providing the error product law (Pass ≤ p^k) to theorize the structural causes of numerical generation failures. A 135M backbone achieves an 87.6% kernel verification pass rate, with a version-frozen verification pipeline plus independent rechecking and reverse verification, and artifacts are public. The problem domain is limited to constructive discrete mathematics, but the architectural paradigm is worth careful digestion.
REU F2F, a Lean 4 benchmark of 244 open problems, shows frontier AI agents resolve only ~42%, revealing a large gap in formalized mathematical research.
Editor's noteThe first benchmark to systematically collect open conjectures from REU undergraduate research projects and formalize them in Lean 4 (244 problems), using a bidirectional prove/disprove protocol and dual kernel verification with Comparator+nanoda, and introducing a unified coding-agent evaluation framework, Leanimum-agent. Compared to Issue 10's Annals dataset (known theorem statements) and Formal Conjectures (community-interest problems), the increment lies in focusing on low-attention open problems to reduce leakage risk, and aligning open-problem evaluation with coding-agent workflows for the first time. Even the strongest models solve only about 40%, leaving clear room for end-to-end open-problem solving. Some results rely on frontier models, but the benchmark's reproducibility design makes it an important artifact for future evaluation.
Structure-Aware Equivalence with Lean-checkable verification separates correctness criteria from proof search, rejecting 100% of logically equivalent but mathematically unrelated reformulations while preserving translation-relevant structure.
Editor's noteProposes structure-aware equivalence (SAE), a role-preserving formal equivalence relation between syntactic equivalence and full logical equivalence, operationalized through the ACE verification framework, providing Lean-verified equivalence/non-equivalence judgments. Compared to Issue 4's ShadowBench (bidirectional implication) and Issue 10's FaithAlign (phrase-level alignment), the increment lies in advancing equivalence judgment from logical equivalence to structural role preservation, explicitly handling premise-conclusion structure and relational content, and rejecting pairs that are logically equivalent but mathematically role-irrelevant (BEq+ accepts 94-96% of irrelevant but mutually provable pairs; ACE rejects all). Has direct value for designing reproducible autoformalization evaluators.
ITPEVAL, the first four-way cross-ITP benchmark, shows library mismatches—not logical foundations—dominate translation difficulty, with type-checking alone overestimating semantic fidelity by nearly half.
Editor's noteThe first cross-system formal translation benchmark spanning Lean 4, Rocq, Isabelle, and HOL Light, covering two logical foundations, with 390 aligned files and 1,700+ theorems, divided into a controlled layer (isolating basic translation difficulty) and an ecosystem layer (exposing library API mismatches). Compared to Babel-formal (Lean-Rocq only), the increment lies in the four-system scope, layered design, and systematic evaluation of 12 directed translation pairs, along with a unified state-isolation verification infrastructure and deterministic BEq semantic equivalence checking, proving that type-checking alone significantly overestimates semantic fidelity (only 54% pass BEq). Data and code are public, making it a reproducible artifact for cross-ITP translation and autoformalization evaluation.
Lean Finder V2 bridges the ambiguity gap in Mathlib theorem retrieval via adversarial training and query rewriting, achieving state-of-the-art Recall@10 of 0.893.
Editor's noteAddresses ambiguous queries in Mathlib semantic search: synthesizes 600,000 labeled ambiguous query-statement pairs via retriever-guided adversarial training, with the same data used for both retriever fine-tuning (model-level) and GEPA-optimized query rewriting (input-level). Compared to Issue 10's Lean Graph Search (multi-hop retrieval using Mathlib's dependency graph) and prior Lean Finder (static intent clusters synthesizing queries), the increment lies in explicitly training against the retriever's current weaknesses to bridge the ambiguity gap, with an LLM gate maintaining alignment. Achieves a relative 14% improvement in Recall@10 on MathlibQR, and downstream proof success improves when integrated with Claude Code. The 600,000-corpus and benchmark are public, making it an actionable contribution to premise selection and agentic workflows.
A three-layer verification stack combining semantic, numerical, and vacuity checks achieves the lowest error rates in Lean autoformalization, catching defects all LLM judges miss.
Editor's noteProposes a verification stack that layers mechanical numerical checks and vacuity checks atop LLM semantic judgments: numerical checks mechanically translate Lean theorems into mpmath evaluation, and vacuity checks detect vacuous proofs from contradictory assumptions by replacing the goal with an opaque conclusion. Compared to Issue 4's Ground False and Beyond Compilation (LLM judgment only), the increment lies in providing a reproducible mechanical check layer that can find defects missed by all LLM judges (e.g., the false Taylor bound in Beyond Compilation, capturable only by numerical checks), and systematically identifying mislabeled and source-defective entries in multiple existing datasets. Achieves the lowest accepted-error rate on three labeled datasets. Focuses on special functions, but the methodology generalizes to other large-scale formalization projects.
AI-generated proofs in Lean diverge structurally from human proofs, with 5.8x greater gesture-mix divergence and only 31% realized compression versus 73% in mathlib.
Editor's noteFor the first time uses proof theory as an empirical measurement tool rather than an optimization target: uses cut elimination and proof compression metrics (gestures, cut compression, compressibility, redundancy) to systematically compare AI-generated proofs with human proofs, accompanied by explicit comparisons of compilation patterns, toolchains, and layouts. Compared to Issue 8's LeanPolish (compressing proofs) and Issue 4's ProofJudge (evaluating quality), the increment lies in shifting from "improving proofs" to "measuring proofs" as a scientific instrument: finds that AI proofs achieve far lower logical compression than human proofs (31% vs 73% in mathlib), and 40% of AI proofs contain redundant intermediate declarations (humans: 13%), providing the first systematic, controlled quantitative evidence for the phenomenon that "AI proofs are longer than necessary." The methodology and open-source repository are valuable for anyone building or evaluating Lean provers.
