AI Just Checked Math’s Longest Proof. Here’s What It Means for Trusting AI Code

Most AI news I write about is AI writing code faster. This week's news was different. Two AI labs announced that their systems hadn't just produced math. They'd produced math a computer could check line by line.

I'm not a mathematician, and I can't judge these proofs. You don't need to either. What matters for anyone shipping software is the pattern: an AI does a huge amount of work, a separate checker verifies it, and people focus on whether the checker was asked the right question. That's where AI-written code is headed too. It's also why I keep saying agents should test what they build and that an eval score isn’t an approval.

The Classification of Finite Simple Groups (CFSG) is the theorem that lists the "atoms" of symmetry. In Axiom’s announcement, the company describes the original proof as roughly 15,000 pages in more than 500 articles by about 100 mathematicians.

Here's what Axiom says happened:

• Over 24 days, its engineers and mathematicians "directed swarms of dozens of AI agents" that produced about 43.1 million lines of Lean, a language where a computer checks every step of a proof.
• Translating the proof exposed problems in the published work. Most were minor, like typos and errors in tables. Axiom counts 34 "noteworthy deviations," the most substantial involving the Unbalanced Group Theorem, which it rerouted with a new argument and an accompanying paper.
• Axiom corresponded with Richard Lyons and Ronald Solomon, two group theorists whose work the classification rests on, and it has posted an errata list for the group theory community.
• The code is public. The README calls it "sorry-free" (no skipped steps) and says the full build takes under 24 hours. The main theorem statement comes from a separate project, TauCeti, not from Axiom.

One correction to the posts going around: the "50 million lines" figure doesn't match Axiom's own numbers. Its site says 43.1 million lines of Lean and 2.05 million declarations. I also didn't find Axiom calling it "the largest computer-verified proof." What it actually says is that this is "the first complete computer-checked proof" of CFSG.

The same day, OpenAI announced three results and asked outside experts to shepherd each one:

• Math: a proof of the local smoothing conjecture in every dimension, which OpenAI says also settles the Kakeya conjecture. It released the AI's write-up and a Lean proof.
• Computer science: OpenAI's exact words are "Surprisingly, our system has recently proved that the ETH is false, a result that was subsequently verified in Lean." More on this one below.
• Physics: an existence proof for certain four-dimensional quantum field theories, including quantum chromodynamics. OpenAI describes the pure Yang–Mills piece as part of a Millennium Prize problem, not the whole problem. The physics group chose not to release the AI's materials yet, so there's nothing public to check.

OpenAI says it isn't seeking academic credit, and that the outside groups work unpaid and independently. The files are in its public math repository.

The Exponential Time Hypothesis (ETH) says 3-SAT, the classic logic puzzle at the heart of P vs. NP, can't be solved in time that grows meaningfully slower than exponentially. A lot of research in computer science is built on the assumption that it's true.

OpenAI's paper gives a deterministic algorithm that counts the solutions to these formulas in subexponential time. If it holds up, that refutes ETH. A few details matter:

• Lean checked a slightly weaker bound. OpenAI's formalization notes say the Lean proof gives a looser time bound than the paper. It's still subexponential, which is what matters for ETH.
• The experts aren't vouching for it yet. The review is led by Russell Impagliazzo and Ramamohan Paturi, who proposed ETH, and Ryan Williams of MIT. Their open letter says: "Our involvement should not be taken as certification of the claim." Williams called it "a claimed refutation of ETH."
• Anthropic posted a similar claim hours later. Late on October 26 (Central), Anthropic published its own Lean-checked paper saying a Claude model found a subexponential 3-SAT algorithm, also on October 16. It says the result "is purely asymptotic and says nothing about solving formulas in practice."

So no, your app didn't get faster, and nobody solved P vs. NP. It's a big claim, it's being checked in public, and it hasn't been confirmed yet.

This is the part that applies directly to code.

A proof checker like Lean is very hard to fool about whether a proof follows from its statement. It can't tell you whether the statement is the one you meant. Axiom puts it plainly: "Humans inspect that statement and the definitions it uses to confirm that it expresses the intended classification; Lean checks the formal deductions establishing it."

The Computational Complexity blog raised the same concern about OpenAI's earlier math release: "Lean might be verifying a proof of a theorem different than what was intended." That's why both labs and the expert groups keep repeating that these results are pending review.

Swap "proof" for "code" and you have the main risk with AI-written software. An agent can write code that passes every test it wrote for itself, and still build the wrong thing. The checks only mean something if someone made sure they test the right behavior.

You don't need Lean to run a small business website. You can borrow the same setup, though: cheap automated checking, plus human attention where it counts.

1. Write the spec before the code. A few plain sentences: what the feature does, what it must never do, and what happens with bad input. That's your theorem statement. Review it more carefully than anything the AI writes.
2. Make the tests the contract. Have the agent write tests from your spec, then read the tests yourself. A wrong test gives you false confidence, and that's worse than having no test.
3. Turn on the free checkers. Strict type checking (TypeScript's strict mode, or PHPStan for PHP), linters and CI that blocks merges on failures. They're the closest thing most of us have to a proof checker, and they don't get tired.
4. Test properties, not just examples. For anything involving money, dates or permissions, check rules that should always hold ("a refund never exceeds the charge"), not just a few hand-picked cases.
5. Save formal methods for the small, critical core. Most sites never need them. If you have one piece where a bug is truly expensive, like payment math or access rules, that's where heavier verification can earn its cost.
6. Keep a human at the gate. Read the spec, the tests and the risky files. Let the machines read everything else.

That last point is the same lesson as PHP2Shell: AI is now good at finding problems in work people trusted for years. Axiom's errata list shows the same thing on a 15,000-page proof. Your codebase is a lot smaller.

I'm not rewriting client sites in a proof assistant. I am leaning harder on the cheap version of this: specs before code, tests I actually read, strict type checks and CI that won't merge red builds. AI writes more of the first draft every month. My job is shifting toward making sure the checks around it are right.

If you're using AI to build or maintain your site or app and want to know whether the tests and checks around it would catch a real mistake, get a free quote. I work with businesses in Nashville and Middle Tennessee and with remote teams. I'll look at what you have and tell you, in plain English, where it's covered and where it isn't.

Did AI really verify the Classification of Finite Simple Groups?
Axiom says its AI agents produced a complete, sorry-free Lean formalization (about 43.1 million lines) in 24 days, with mathematicians directing the work. The code is public. I haven't seen an independent review yet. The key question for reviewers is whether the formal statement matches the classical theorem.

Did OpenAI disprove the Exponential Time Hypothesis?
OpenAI says its system did, and that the result was checked in Lean. The expert group reviewing it says its involvement "should not be taken as certification." Treat it as a serious claim that's still pending. Anthropic has posted a similar claim.

Does this make my software faster?
No. Both ETH papers are about asymptotic running time. Anthropic says its result says nothing about solving formulas in practice, and OpenAI says turning it into practical improvements will take significant further research.

What is Lean?
A programming language and proof assistant where a computer checks every step of a mathematical proof against its stated theorem.

Should my business use formal verification?
Probably not for most of your code. Clear specs, tests you've read, strict type checks and CI catch most real problems. Save formal methods for small, critical pieces.

• Axiom, “Formalizing the Enormous Theorem” (Oct 26, 2026)
• Axiom, CFSG in Lean site (43.1M lines, 2.05M declarations)
• AxiomMath/CFSG on GitHub
• OpenAI, announcement of three new results and outside review groups (Oct 26, 2026)
• OpenAI math repository, release history (Oct 26 entry)
• OpenAI, Lean formalization scope for “The Exponential Time Hypothesis is False”
• Impagliazzo, Paturi and Williams, open letter to the community
• Ryan Williams on Bluesky (Oct 26, 2026)
• Anthropic, “A 2^o(n) Time Algorithm for 3-SAT” (paper and Lean)
• Computational Complexity blog, “AI, Math, the document-drop. Non-Tech Thoughts” (Oct 18, 2026)
• Lean
• Harmonic, “Aristotle Expands Into Formal Verification for Software and Hardware, Starting With C and Verilog” (Oct 27, 2026)
• Harmonic, Aristotle overview and case studies on LibTomMath and Tensordyne
• Reuters via KSL.com, “Robinhood CEO's AI startup Harmonic expands into software, chip design verification” (Oct 27, 2026)