Write It, Then Prove It: AI That Checks Its Own Work With Math

On September 4, 2026, Kevin Buzzard, a mathematician at Imperial College London, wrote a blog post with an unusual title: “FLT: Anthropic has beaten me to it.”

FLT is Fermat’s Last Theorem, the famous claim that no whole numbers a, b and c satisfy aⁿ + bⁿ = cⁿ for any n bigger than 2. Andrew Wiles proved it in the 1990s. Since 2024, Buzzard has led a funded project to write a version of that proof in Lean, a programming language in which a computer can check every step of a mathematical argument.

Anthropic had just announced that dozens of Claude agents, running an unreleased internal research model, had produced a complete Lean proof of the theorem in 11 days, with occasional high-level direction from one researcher. According to Anthropic, the result is about 13 million lines of Lean, more than five times the size of Lean’s whole shared maths library, and it was built on that library and on pieces of earlier human projects, including Buzzard’s.

Buzzard compiled it himself and ran an independent checking tool on it. His verdict: “it checks out.”

He also wrote that the work “tells us essentially nothing” new about mathematics. He was already about 99.9% sure the proof of FLT was fine. What was new was the method: a machine wrote millions of lines of argument that no human will ever read, and that didn’t matter, because a different, much smaller program checked every line.

That’s the idea this post is about. Language models write fluently and are often wrong. So let them write freely, and then make a strict checker decide whether what they wrote is actually true.

Why checking beats trusting

You’ve probably seen a language model state something false with complete confidence: a citation that doesn’t exist, a function that isn’t in the library. This is usually called hallucination, and it comes from how these models work: they produce the most plausible next words, and plausible isn’t the same as true.

There are two ways to deal with that. You can try to make the model more trustworthy, which helps, but never gets you to certain. Or you can stop trusting it and check its output with something that can’t be fooled by fluency.

I’ve argued for the second approach in ordinary software too: treat the LLM like an unreliable API, and validate everything it returns.

Formal verification takes that idea to its limit. The loop looks like this:

1. Write the question precisely, in a formal language a computer understands. This precise version is called the specification, or spec.
2. Let the AI generate a proof (or a program plus a proof) as freely as it likes.
3. Run the checker. If every step follows from the rules, accept. If not, the checker says where it failed.
4. Retry with that error message, as many times as you can afford.

Why the checker deserves trust

The checker in this loop is not another AI. It’s a fairly small, carefully written program.

Proof assistants like Lean follow what’s often called the de Bruijn criterion, after the Dutch mathematician Nicolaas de Bruijn: however big the rest of the system is, every finished proof must be checked by a small trusted kernel that applies a handful of logical rules. The AI can be wildly wrong. Nothing counts as proven until the kernel accepts it.

It’s small enough that people have written independent checkers for Lean, such as Lean4Lean, which can re-check the whole of Mathlib, Lean’s main maths library.

Tests are a weaker version of the same idea

If you write software, you already do a version of this. Tests are checks the code must pass, and as I wrote in Tests Are How You Talk to the AI, they’re the clearest way to tell an AI coding tool what “done” means.

But a test only checks the cases you thought of. A formal proof checks every possible input. The difference matters more than it sounds.

I saw it in my own research notes. In a live test of a small code writer, I gave it three examples that were meant to say “return the most common word”. It produced a program that passed every check. It was also the wrong program: it returned the longest word, which happened to be the most common word in all three examples.

The checks were fine. The examples just didn’t say what I meant. That turns out to be the main catch of this whole approach.

Lean in plain words

A normal maths proof is written for humans. It skips “obvious” steps and is checked by referees, who are good but human, and long proofs are hard to check.

A formal proof skips nothing. Every definition is written out exactly, and every step must follow from earlier steps by rules the computer knows. Writing one is a bit like programming: you state a theorem, write the proof, and the system either accepts it or shows you an error.

Lean is one of several proof assistants (others include Isabelle and Rocq). It has become the favourite for AI work, largely because of Mathlib, a shared library built by volunteers. Its statistics page currently lists about 140,000 definitions and 292,000 theorems from 772 contributors. A model proving something new needs those basics already in place.

Before AI, formalization was slow, careful human work, but it was already reaching research mathematics. In late 2023, Terence Tao, one of the world’s best-known mathematicians, organized a project with Yaël Dillies to formalize a new result he had just proved with Timothy Gowers, Ben Green and Freddie Manners (the “polynomial Freiman-Ruzsa conjecture”). It was done in about three weeks. In 2024 and 2025, his Equational Theories Project used Lean, many contributors and automated tools to settle over 22 million implications between 4,694 simple algebraic laws.

Where AI comes in

AI helps in two main ways.

Proof search. Given a formal statement, a model suggests the next proof step, or a whole proof. Lean says yes or no. The model tries again. Because Lean’s verdict is reliable, you can generate thousands of attempts and keep only the ones that pass.

Autoformalization. Translating ordinary maths (or an ordinary request) into the formal language. This is the step that turns “prove this theorem from the paper” into a Lean statement the checker can work with. It’s also where mistakes slip in, as we’ll see.

The milestones, with their caveats

AlphaProof, July 2024. Google DeepMind’s AlphaProof, working in Lean, plus AlphaGeometry 2 for the geometry problem, scored 28 out of 42 on the 2024 International Mathematical Olympiad (IMO), equal to the top of the silver-medal range. The gold threshold was 29. The proofs were scored by Timothy Gowers and Joseph Myers. Two important caveats, both from DeepMind’s own post: humans manually translated the problems into Lean first, and while one problem was solved in minutes, others took up to three days, compared with two sessions of 4.5 hours for students. The full paper appeared in Nature in November 2025.

IMO 2025: the plot twist. A year later, Google DeepMind reported that an advanced version of Gemini Deep Think scored 35 out of 42, a gold-medal score, certified by IMO coordinators. OpenAI reported the same score for an experimental model, graded by three former medallists it hired. Both worked in plain natural language, within the 4.5-hour time limits, with no Lean at all. DeepMind itself pointed out the contrast with 2024’s translation step.

So for competition maths, plain language models caught up with the formal approach. But formal systems reached the same level too. ByteDance’s Seed-Prover reported fully proving 5 of the 6 IMO 2025 problems in Lean (the paper notes some were finished after the contest window), and Harmonic’s Aristotle reported gold-medal-equivalent performance with formally verified solutions (geometry was handled by a separate solver, outside Lean).

The difference between those two kinds of gold is the whole point of this post. A natural-language proof needs expert humans to grade it. A Lean proof grades itself.

Benchmarks moved fast

Two standard test sets show how quickly AI provers improved:

These are each lab’s own numbers, and as I explained in AI Benchmarks and Goodhart’s Law, benchmarks lose meaning once everyone optimizes for them. But formal benchmarks have one advantage: no lenient grader. Either Lean accepted the proof, or it didn’t.

Beyond maths: software you can prove

Proofs aren’t only for theorems. You can also prove that a program does what its spec says, for every input.

This has a long, mostly human-written history:

• seL4, an operating system kernel, was proven correct in 2009. Its 8,700 lines of C were shown to always follow an abstract specification of how the kernel should behave. The proof took about 200,000 lines of Isabelle and, by the team’s own count, about 20 person-years, including tool building (11 for the seL4-specific proof). It assumed the compiler and hardware were correct.
• CompCert, a C compiler, comes with a proof that the code it produces behaves like the source program. In 2011, University of Utah researchers threw random programs at many compilers with a tool called Csmith and found over 325 bugs. CompCert was the only one where about six CPU-years of trying found no wrong-code errors, although they did find bugs in its unverified front-end parts.
• Amazon Web Services uses automated reasoning at large scale. Its Zelkova engine checks access-control policies by turning them into logic problems, and AWS has described it as handling over a billion such queries a day. In August 2025, AWS made Automated Reasoning checks generally available in Bedrock Guardrails: you write your business rules as a formal policy, and model answers are checked against it. AWS advertises “up to 99%” verification accuracy, which is its own figure for its tested domains, not a general hallucination rate.

Languages such as Dafny and Verus (for Rust) let you write code together with its spec, and a checker confirms they match.

AI writing code and proofs together

In September 2025, a group from the Beneficial AI Foundation and MIT published a benchmark for what they called “vericoding”: given a formal spec, write code plus a proof that the code meets it. It has 12,504 specs. Using off-the-shelf models, they reported success rates of about 82% in Dafny, 44% in Verus and 27% in Lean. Inspecting successful solutions by hand, they found roughly 9% of those specs were too weak to say what was intended, which is a useful reminder that even a benchmark of specs has spec problems.

The obvious next step is to reverse the usual workflow: instead of an AI writing code and a human reviewing it, the human reviews a short spec, and the AI writes code plus a proof that it meets the spec.

The catch: a proof only proves what you stated

A checker answers one question: does this proof prove this statement? It can’t answer: is this the statement you meant?

That gap has a name in software: the spec problem. My code-writing example above is the small version. Three examples were the spec. They allowed two different programs, and the system found the wrong one. A formal spec is far more precise than three examples, but the same thing can happen: if you leave out a condition, or state the wrong one, a perfect proof of the wrong thing is still a perfect proof.

Buzzard said this plainly in a February 2026 post about AI and Lean. If a definition is garbled, the code will still compile; it just won’t mean what it should. His summary: formal languages can check proofs, but humans need to check definitions. He also warned that language models, eager to please, will try to prove a theorem even when it’s false.

That’s why, in the FLT story, the checking had two parts. Lean checked the 13 million lines. Separately, a comparison tool confirmed the final theorem matched the statement of FLT already in Mathlib, and Buzzard read that statement himself. The statement is the part a human must read.

The spec problem cuts both ways, though. In August 2026, Buzzard’s group released the “Annals Challenge”: Lean statements of 50 recent theorems from the Annals of Mathematics, one of the field’s top journals. Writing them precisely exposed several published main theorems that were trivially false as printed, because of small omissions such as a missing assumption that a number is at least three, or that a set is non-empty. Four were in papers by Fields Medallists. Formal statements don’t only catch AI mistakes. They catch ours.

The other costs

• Autoformalization errors. Translating real questions into formal ones is itself done more and more by AI, which brings back the original problem one level up. Benchmarks now add human review for this. Epoch AI’s FrontierMath Erdős benchmark (2026) asks models for Lean proofs of 68 open problems; 17 of the statements were autoformalized, and each was reviewed by Thomas Bloom, who runs the Erdős problems website, to confirm it matches the original.
• Missing foundations. Lots of mathematics can’t be stated in Lean yet because the definitions don’t exist. The Annals Challenge post estimates that only about 20% of Annals papers since 2020 have been formalized, mostly because of missing definitions.
• Cost and speed. The FLT proof took 11 days of many agents working in parallel, and Anthropic itself says it’s likely much longer than it needs to be. AlphaProof needed days per hard problem. Formal proof is getting cheaper fast, but it’s not free.
• Most code has no spec. seL4 and CompCert are famous partly because they’re rare. The great majority of real-world software has tests at best, and no formal description of what it should do. “Prove it correct” first requires someone to say what correct means.

Why this matters for AGI

A grader that never gets tired

The biggest recent change in AI training is reinforcement learning on checkable problems. A model tries a problem, an automatic checker says right or wrong, and the model is trained to do more of what worked. The Tülu 3 paper from the Allen Institute for AI named this in November 2024: reinforcement learning with verifiable rewards (RLVR). DeepSeek-R1 used the same idea at scale in January 2025, with maths answers and code tests as the checkers. I covered that story in Bet #5: Teach It to Think.

The key word is verifiable. Without a checker, a human has to grade every attempt. With one, a system can practise millions of times on its own. AlphaProof is the clearest example: it learned by attempting millions of formal problems, with Lean as the only grader.

That’s why this approach works best in maths and code: those are the areas with good checkers. “Is this a good business plan?” has no Lean.

A grader that’s hard to fool

There’s a second reason. When you train an AI against a reward, it looks for the easiest way to get that reward, including ways you didn’t intend. I wrote about this in Reward Hacking: When AI Wins the Wrong Game. Test suites and AI judges can be gamed.

A proof checker is much harder to game. There’s no “looks convincing” in Lean, and a small kernel leaves little room to exploit. But only if the spec is right. If the statement is subtly wrong, an optimizer will find the gap and “prove” the wrong thing perfectly, and the checker will happily approve it. The weak point moves from the grader to the spec. It doesn’t disappear.

What it means for self-improving agents

This is also why I find the approach interesting for my own research. In my RIAI Lab Notes, I’m working on a terminal agent that writes its own Python code to grow new skills. Right now, its checks are tests run in a sandbox, and the live test above showed the limit of that: a program can pass every check and still be the wrong one. Whether stronger, spec-like checks could let an agent like that learn safely from its own attempts is an open question for me, not something I’ve shown.

The broader point for AGI: a system that can check its own work can improve without waiting for a human to grade it. In maths, that’s becoming real. For most of what we’d want from a general intelligence, the checker doesn’t exist yet, and building one means writing down, precisely, what we actually want. That turns out to be one of the hardest problems there is. (For the bigger picture of where AI stands, see AGI: Where We Are Now, and for why the word itself is slippery, What Does “AGI” Even Mean?)

Where things stand (October 2026)

Only dated, sourced facts here:

• Formalizing big known results has become possible. Anthropic announced a complete Lean proof of Fermat’s Last Theorem on September 4, 2026, produced mostly by Claude agents in 11 days, compiled and checked by Kevin Buzzard. It verifies existing maths; it doesn’t add new maths.
• AI is resolving some open problems, with Lean proofs. A Google DeepMind paper from May 2026 reports that its best formal proof-search agent resolved 9 of 353 open Erdős problems (a famous collection of problems posed by Paul Erdős), at a cost of a few hundred dollars each, and proved 44 of 492 conjectures from the OEIS, a large database of integer sequences. These are the authors’ own numbers, and most of the problems remained unsolved.
• Claims in words still get caught out. In October 2025, an OpenAI executive posted that GPT-5 had “found solutions” to 10 open Erdős problems. The model had actually found existing papers that already solved them, and the post was deleted. Demis Hassabis of Google DeepMind replied: “this is embarrassing.” A Lean proof comes with its own check, which is why newer Erdős benchmarks require one.
• The people closest to it are cautious about quality. An October 2026 guest post on Buzzard’s blog, co-written by Jeremy Avigad, Buzzard and others, argues that large-scale formalization, including by AI, has to be done carefully, and puts it bluntly: a lousy formalization is worse than none.

My own read, as opinion: formal checking won’t make AI trustworthy in general, because most of life has no spec. But wherever we can write down exactly what we want, it changes the question from “do I trust this model?” to “do I trust this statement?” The second question is much smaller, and humans can actually answer it.

Key ideas

• Language models write fluently but unreliably. Formal verification stops trusting them and checks instead: write freely, check strictly.
• A proof checker is a small trusted program. If it accepts a proof, the proof is correct, no matter how unreliable the AI that wrote it.
• Tests check the cases you thought of; proofs check every input. That’s a big step up, but not the last step.
• A proof only proves what you stated. The spec is where errors hide, so humans still need to read and check the statement.
• Checkers make self-improvement possible. Reinforcement learning with verifiable rewards lets a system practise without a human grader, which is why progress is fastest in maths and code.
• Verifiers resist reward hacking only if the spec is right. A wrong spec gets “proven” perfectly.
• As of October 2026, AI has formalized Fermat’s Last Theorem and resolved a handful of open problems with Lean proofs, while most real software still has no formal spec at all.

Sources: Kevin Buzzard, FLT: Anthropic has beaten me to it (Xena Project, September 2026); Anthropic, Formalizing Fermat’s Last Theorem (September 2026); Kevin Buzzard, Accelerating mathematics (Xena Project, February 2026); The Annals Challenge (Xena Project, August 2026); How to Formalize All of Mathematics (Xena Project, October 2026); Lean4Lean: Verifying a Typechecker for Lean, in Lean (arXiv); Mathlib statistics; Xena Project, Lean in 2024 (on the PFR formalization); The Equational Theories Project (arXiv, December 2025); Google DeepMind, AI achieves silver-medal standard solving IMO problems (July 2024); Hubert et al., Olympiad-level formal mathematical reasoning with reinforcement learning (Nature, 2025); Google DeepMind, Gemini Deep Think IMO 2025 gold; Simon Willison on OpenAI’s IMO 2025 result; Seed-Prover (arXiv, July 2025); Aristotle: IMO-level Automated Theorem Proving (arXiv, October 2025); DeepSeek-Prover-V2 (arXiv, April 2025); Klein et al., seL4: Formal Verification of an OS Kernel (SOSP 2009); Yang et al., Finding and Understanding Bugs in C Compilers (PLDI 2011); Amazon Science, A billion SMT queries a day; AWS, Automated Reasoning checks now available (August 2025); Bursuc et al., A benchmark for vericoding (arXiv, September 2025); Lambert et al., Tülu 3 (arXiv, November 2024); Tsoukalas et al., Advancing Mathematics Research with AI-Driven Formal Proof Search (arXiv, May 2026); Epoch AI, FrontierMath Erdős; TechCrunch on the GPT-5 Erdős claims (October 2025).

Related: Bet #5: Teach It to Think (Reasoning and Agents), Reward Hacking: When AI Wins the Wrong Game, and Tests Are How You Talk to the AI.