Issue 1: Neural Theorem Proving Enters Open Research Problems, Kernel Soundness and Benchmark Reliability Take Center Stage
Highlights of This Issue
The most central signal this issue is that neural theorem proving has officially moved from competition problems to open research problems. In AlphaProof Nexus, an agentic framework autonomously solved 9 of 353 open Erdős problems (including two that had been open for 56 years) and 44 of 492 OEIS conjectures in Lean 4; more importantly, its ablations show that a naive agent of "LLM generation + Lean compiler feedback" performs comparably to the full agent equipped with evolutionary search and AlphaProof tools on most problems. The validity of this evaluation relies on the 2,615 formalized propositions (including 1,029 zero-contamination open conjectures) and frozen evaluation subsets provided by Formal Conjectures—it is becoming the de facto standard for research-grade formal benchmarks.
Another main thread is "reliability": both the reliability of benchmarks themselves and the reliability of the kernel itself. Faults in Our Formal Benchmarking conducted a corpus-level audit of five mainstream Lean benchmarks, finding 4,833 problems, of which 398 are mechanically verifiable defects, and demonstrated that defects can both inflate and deflate prover scores. Meanwhile, the community digested a Lean 4 kernel soundness vulnerability—where projections of nested inductive types could forge 0=1 without axioms, fixed in v4.33.0, with Leonardo de Moura's postmortem analysis providing a rare root cause and fix case study. Together, these two events remind us: "kernel acceptance" is a necessary but not sufficient condition.
On automated formalization quality assessment, multiple works converge on the gap of "compilation success ≠ semantic fidelity": Theo's type-first paradigm, Faithfulness Gap's bidirectional provability fingerprints, and Beyond Compilation's consensus LLM-as-judge metrics, each advancing evaluation from "can compile" to "semantically equivalent" from different angles. Meanwhile, MechGeo shows that Euclidean geometry can now be systematically tackled, jumping from 2/14 to 12/14 on Lean-IMO-Bench.
Community and Developments
- Lean 4 kernel soundness vulnerability: oss-security disclosed a class of vulnerabilities that could forge axiom-free proofs of 0=1 via projections of nested inductive types, affecting all versions ≤ v4.31.0, fixed in v4.33.0; Leonardo de Moura's postmortem analysis points out this is an implementation defect rather than a metatheoretical flaw, and emphasizes the value of independent kernels (such as nanoda). Any team relying on Lean-verified artifacts (especially LLM-generated proofs) should re-verify with --trust=0.
- Annals Challenge: Xena Project released Lean 4 formalizations of 50 important theorems from the Annals of Mathematics since the 2020s (proofs left as sorry), covering about 20% of Annals papers, and has been made available on lean-eval. Its core argument is: current mathlib lacks many modern mathematical definitions, so even if AI can prove, it has no way to state them—this directly points to the bottleneck in formalization library development.
- Zeta23: An analytic number theory result independently discovered by a large language model and accompanied by Lean 4 formalization, improving the lower bound on the proportion of zeros on the critical line from 41.6% to 2/3, with improvements on the proportions of simple zeros and distinct zeros. As a landmark case of "LLM discovery + formal verification" integration, its verification process is worth attention.
Open Questions
- The naive agentic loop (LLM + compiler feedback) is sufficient on most open problems, but do the hardest open problems still require the full architecture with evolutionary search and AlphaProof-like tools? Where is the boundary where "simple loops fail"?
- Can the gap of "compiles but unfaithful" be truly closed—through stronger semantic verification, better formalization feedback, or fundamentally different semantic anchoring?
- Kernel soundness vulnerabilities show that even mature kernels may have subtle defects: how should the community incorporate independent kernel verification (nanoda-style) into the trust chain for AI-generated proofs, making it the default rather than the exception?
Papers in this issue
An AI proof agent using Lean formal verification autonomously solved 9 open Erdős problems and 44 OEIS conjectures, with simple LLM feedback loops rivaling complex evolutionary systems.
Editor's noteThe first large-scale evaluation of LLM-driven formal proof search on open research-level problems: autonomously solving 9 open Erdős problems (including two open for 56 years) and 44 OEIS conjectures in Lean 4. The key increment is that ablation experiments show the basic agent of "LLM generation + Lean compiler feedback" performs comparably to the full agent on most problems, and all proofs and cost analyses are publicly available, making it essential reading for understanding current agent design trade-offs.
Formal Conjectures provides 2,615 Lean 4 formalized problems including 1,029 open conjectures, creating a zero-contamination benchmark where AlphaProof proves 50% and DeepMind agents 66% of solved statements.
Editor's noteProvides 2,615 Lean 4 formalized propositions (including 1,029 zero-contamination open conjectures and 836 solvable propositions), along with frozen evaluation subsets and a misformalization taxonomy, directly addressing the data leakage and saturation issues of MiniF2F/PutnamBench. As the vehicle for systems like AlphaProof Nexus to solve open problems, it has become the de facto standard for research-grade formal benchmarks, worth reading for anyone working on neural theorem proving or automated formalization.
MechGeo proves 29 IMO geometry problems and refutes 14 flawed formalizations via Lean-verified counterexamples, achieving 43 total faithful proofs through repair.
Editor's noteProposes the GeoIR deterministic intermediate representation and the selective algebraization prover GeoProver, unifying automated formalization and proving of Euclidean geometry into Mathlib-native Lean 4. It jumps from the previous best 2/14 to 12/14 on Lean-IMO-Bench, and completes the remaining propositions through counterexample-guided repair of missing non-degeneracy conditions, with all code and proofs publicly available, marking a reproducible milestone in geometry formalization.
Auditing 10,000 Lean theorem-proving benchmark problems reveals 398 mechanically certified defects that both inflate and deflate prover scores, invalidating benchmarks as self-verifying.
Editor's noteThe first corpus-level defect audit of mainstream Lean benchmarks including miniF2F, ProofNet, FormalMath, CombiBench, and ProverBench, proposing a defect taxonomy and implementing a static checker as a Lean 4 metaprogram, finding 4,833 issues in total. It demonstrates that defects can both inflate and deflate prover scores, and releases a reusable checker and corrected snapshots, crucial for anyone relying on these benchmarks for evaluation.
Theo, an agentic framework using general-purpose coding LLMs, autoformalizes research mathematics into Lean 4, proving 32/32 sampled Putnam problems and catching a false lemma in a published STOC paper.
Editor's noteProposes a type-first automated formalization paradigm: the orchestrator explicitly defines missing domain types before formalizing the main theorem, and uses provable auxiliary lemmas as "unit tests" for verification, thereby breaking through Mathlib's existing coverage. It successfully formalizes seven research papers (including five STOC papers, two with axiom-free proofs), and exposes a gap in a published STOC proof, representing a real increment in handling research-level mathematical automated formalization.
Bidirectional Provability Fingerprinting detects 89.6% of semantically drifted autoformalizations at 3% false positives, outperforming typechecking and LLM-judge baselines by over 40%.
Editor's noteProposes the Bidirectional Provability Fingerprint (BPF) framework, using forward/backward consequence neighborhoods for reference-free semantic equivalence certification of natural language and formal propositions, and releases the first DriftBench benchmark with controlled drift annotations (2,183 pairs). It advances automated formalization evaluation from heuristics like typecheck/BLEU/back-translation to principled semantic equivalence checking, with direct value for building trustworthy formalization pipelines.
A multi-agent LLM system autonomously formalized the fundamental theorem of matrix-product states in Lean 4, discovering a novel proof via Skolem-Noether and building a 227,000-line tensor-network library.
Editor's noteThe first autonomous formalization of research-level theorems in theoretical physics (fundamental theorems of matrix product states) using multi-agent coordination, persistent memory, and blueprint guidance, at a scale of 62k lines and 2,300 declarations. The honest documentation of forced failure modes for "mathematical intent" (doubly stochastic normalization weakening, finite-to-asymptotic replacement) is valuable experience for anyone doing agentic formalization, and the TNLean library and review reports are all publicly available.
FORMATHEORIA formalized the Classification of Finite Simple Groups in Lean at 994,000+ lines, exposing source defects and achieving 4.2x speedup via dependency-aware parallelism.
Editor's noteA large-scale end-to-end AI-assisted formalization workflow targeting the Classification of Finite Simple Groups (CFSG), reconstructing a coherent theory from heterogeneous literature at a scale of 994k lines and 30k declarations through recursive dependency discovery, cross-source alignment, and review-gated termination. Its increment lies in constructing and expanding the formalization context itself rather than merely proving given propositions, and it includes ablation analyses of parallelism and context sharing.
Tool-augmented agents reach 89.5% compilation but only 60.5% semantic faithfulness, exposing a 29-point gap where Lean-valid statements misrepresent the original theorem.
Editor's noteProposes human-calibrated consensus LLM-as-judge metrics, distinguishing compilation validity from semantic fidelity, and uses a 2^3 factorial design to decompose the roles of drafting, searching, and refinement feedback. The core finding is that refinement feedback widens the "compiles but unfaithful" gap (by 29 percentage points), while searching mainly improves selectivity rather than final fidelity, providing actionable attribution conclusions for designing formalization agents.
