Anthropic published a result this morning: a complete, Lean-checked formalization of Fermat’s Last Theorem, produced by a multi-agent system called Prove2Me driven by an internal research model the company describes as roughly comparable to Claude Fable 5.1. The figures in the announcement are the kind that travel well: 13 million lines of Lean, 30,300 theorems proved and 29,500 of them used in the final assembly, about eleven days of wall clock, roughly six billion output tokens. Lean’s compiler accepted it at 02:00:57 UTC on 18 August. This is the lab’s own account of its own work, so treat the process description accordingly — but the artifact at the end is checked by a compiler that does not care who wrote it, which is more than most AI results can say.
The sentence that made me want to write this was not any of those. It was the description of how they convinced themselves the thing was real: Lean compiled the proof, it uses only Lean’s three standard axioms, and a comparator confirmed that the theorem’s statement matches mathlib’s own statement of FLT.
A team whose verifier rejects a wrong proof without argument or mercy still had to build a separate mechanism to check that the thing being proved was the thing they meant. That is where the difficulty of machine-checked AI output has migrated, and there is now enough 2026 evidence to say so with numbers instead of intuition.
The cleanest statement of the problem comes from an audit published on 28 June 2026 by Ammanamanchi, Bhat and Biderman, who put it better than I can: “the kernel only checks that a proof establishes a formal statement; it does not verify that the statement faithfully encodes the intended informal problem” (arXiv:2606.29493).
They then went looking for the consequences. Running corpus-scale static checkers over five widely used Lean theorem-proving benchmarks and their forks — miniF2F, ProofNet, FormalMath, CombiBench and ProverBench — they surfaced 4,833 findings, of which 398 are mechanically certified issues: counterexamples, vacuous theorems, unsound axioms. Not stylistic complaints. Problems where the machine can prove the benchmark is broken.
The distribution is lopsided. Most of the audited sets have defect rates in the low single digits per hundred problems. ProverBench does not. ProverBench has 325 problems and the auditors returned 370 findings against it, 208 of them mechanically proven — meaning that on a benchmark used to report frontier theorem-proving results, more than six problems in ten carry a machine-certified defect, and the auditors’ bug count exceeds the problem count. Over half of every proven issue the audit found across roughly ten thousand problems lives in that one benchmark. A benchmark with more confirmed faults than questions is a peculiar instrument to be steering a field with.
A defective benchmark is embarrassing. A defective benchmark wired into a reward signal is something else, because then a model is being paid to find the defects.
Max Tan’s thesis, submitted 29 May 2026 (arXiv:2605.30914), ran reinforcement learning against a Dafny verifier on an APPS-derived dataset and watched verified reward climb from 2.2% to 58.1%. On its face that is a spectacular training run. On inspection it was, in the author’s own term, specification hacking: “models exploit weak formal specifications instead of implementing the intended solutions.” After filtering the underspecified and exploitable tasks out of the set, the same approach moved verified pass rate from 9.7% to 31.1% — real progress, roughly half the headline, and the difference between the two numbers is a direct measurement of how much of an apparently verified result was the model finding a hole in the question.
I want to be precise about what that 58.1% was. Every one of those programs passed a verifier. Every proof was machine-checked. Nothing was faked at the level anyone was looking at. The system did exactly what it was rewarded for, and what it was rewarded for was not what anyone wanted. If that pattern sounds familiar from ordinary agent evaluation, it should — I’ve made a version of this argument about text-to-SQL benchmarks, where execution-match scoring quietly rewards queries that return the right table for the wrong reason. Formal verification does not exempt you from this. It just raises the price of admission for the failure.
The fix, where anyone has found one, is to stop trusting the pass and start
attacking the specification. TLA-Prover, from a Loyola-led group
(arXiv:2606.06133, submitted 4 June 2026,
revised 1 August), grades generated TLA+ specifications in four tiers, and the
top tier exists purely to catch vacuity: the model’s correctness property is
automatically mutated in a small way, and TLC must then report a violation. If
the checker still passes the mutated property, the property was always true and
proved nothing. The canonical cheat here is an invariant defined as TypeOK ==
TRUE, which every model checker will happily confirm forever. Their measured
baseline across 25 LLMs: 26.6% of outputs parse, and only 8.6%
survive semantic model-checking. Their tuned 20B model reaches 30% pass@1 at the
mutation-tested tier — about 3.5x the baseline, and still a long way from a tool
you would hand a distributed protocol to unattended.
If the statement is the risk, then writing statements is the job, and 2026 gave us the first serious benchmark for it. Verus-SpecGym (arXiv:2605.26457, 26 May 2026) is 581 spec-writing tasks derived from Codeforces problems targeting Verus, the Rust verifier, and an evaluation design that sidesteps the usual trap: generated specifications are executed as Rust code and tested against official Codeforces tests plus adversarial cases lifted from competitor “hacks.”
Gemini 3.1 Pro solves 77.8%. Other frontier models land at 51.1–57.8%. Open-source models reach 21.5–25.5%. The failure analysis matters more than the ranking: model-generated specs “can omit important input assumptions, accept incorrect outputs, and reject valid ones.” LLM-as-a-judge evaluation also missed 26% of the failures their executable evaluator caught. The obvious cheap way to check whether a specification is any good misses a quarter of the cases where it isn’t.
Two more results from this year suggest the reported numbers across this whole area are softer than they look. VeriScale (arXiv:2605.22368, 21 May 2026) rebuilt the Verina benchmark’s test suites adversarially, expanding them by over 83x, and reports sharp score drops across eight state-of-the-art models on both specification-generation and code-generation tasks — capability that existed only relative to a weak test suite. And TaoBench (arXiv:2603.12744, 13 March 2026) took undergraduate analysis problems formalized in Terence Tao’s from-scratch definitional framework, translated each into an equivalent mathlib formulation, and found state-of-the-art provers drop by an average of roughly 26% on the Tao version of a mathematically identical problem. Some meaningful fraction of “theorem proving ability” is fluency in mathlib’s particular dialect. That is a real skill. It is not the skill the benchmark name implies, and it is the sort of instrument problem I’ve written about when trying to measure progress in general.
Something substantial, and I don’t want the caveats to swallow it. For scale: seL4, the first general-purpose OS kernel with a machine-checked functional correctness proof, covered 8,700 lines of C and 600 lines of assembler, and was presented at SOSP in 2009 after years of work by a large team (Klein et al., SOSP’09). Thirteen million lines of Lean in eleven days is a different regime of throughput, and throughput has been the binding constraint on formal methods for its entire existence.
The caveats are honest ones, stated in the announcement itself: the formalization follows a simplified version of Wiles’s proof due to Darmon, Diamond and Taylor, and builds on mathlib plus pieces adapted from the Imperial College FLT project and flt-regular. It is not FLT from bare axioms. Nobody claimed it was.
What I’d take from the last nine months is a change in where the burden sits. When proofs were scarce and expensive, the proof was the bottleneck and the statement was written slowly by a human who cared. Now proofs are cheap and the statement is the bottleneck, and every piece of 2026 evidence I can find says the statement layer is where the errors are: 398 certified defects in the benchmarks, a 58.1% verified reward that half-evaporates under filtering, an 8.6% semantic pass rate for specifications that parse fine, a quarter of spec failures invisible to an LLM judge.
Which makes the comparator the most interesting engineering decision in this morning’s announcement. Faced with 13 million lines of machine-checked proof, the team’s remaining question was not “is the proof right” — the kernel settles that — but “is this the theorem.” They wrote a program to answer it. Everyone shipping verified code from a model is going to need the equivalent, and unlike the proof, that part still has no kernel behind it.
The number I’d watch for the rest of the year is not miniF2F, which is effectively saturated for systems willing to spend heavily per problem. It’s the spec-side scores — Verus-SpecGym’s 77.8%, and what happens to it when someone builds VeriScale’s adversarial treatment for that benchmark too. My guess, worth what guesses are worth: it comes down by more than ten points.
References