Table of Contents
Verify AI Math Proof: How Mathematicians Check 125 Pages
How experts verify AI math proof claims: human refereeing, Lean formalization, and repeated runs. Why a 50% success rate changes what checking means for kids.
Learning to verify AI math proof output has become a real job, and the reason is arithmetic. A model can generate a hundred pages in an afternoon. A human referee reads mathematics at a few pages an hour, slowly, with a pencil. When the May 2026 unit distance result came out, OpenAI said external mathematicians checked it and wrote a companion paper. That worked because the result mattered enough to get four serious mathematicians’ attention.
Most AI-generated proofs will not get that. Thomas Bloom, who maintains the Erdős problems database, described the flood to Quanta: papers of 100 to 200 pages arriving as claimed solutions where “no human has read it.”
Key Takeaways
- Three verification routes exist: human refereeing, formal verification in a proof assistant, and repeated sampling. Each answers a different question.
- Human refereeing is the gold standard and does not scale. Reading a proof is roughly as hard as writing one.
- Formal verification in Lean is mechanically certain but requires translating the informal argument into the system, which is itself substantial work.
- Repeated runs measure reliability, not correctness. OpenAI reported about a 50% success rate on the unit distance problem across identical prompts.
- The Liquid Tensor Experiment showed formalization can work at research level: Peter Scholze’s challenge, posed December 2020, was completed in Lean by July 2022.
What it takes to verify AI math proof claims
A mathematical proof is a chain of logical steps where every step follows from previous ones and from accepted axioms. Verification means confirming that no step is broken. That is harder than it sounds, because a single invalid inference anywhere invalidates the conclusion, and invalid inferences can be subtle.
For the unit distance result, OpenAI’s account says the proof “has been checked by a group of external mathematicians” who “also written a companion paper explaining the argument and providing further background and context.” Those mathematicians included Noga Alon of Princeton, Tim Gowers, Arul Shankar, Jacob Tsimerman, and Thomas Bloom. Gowers, a Fields medalist, wrote that had a human submitted the paper to the Annals of Mathematics and asked his quick opinion, “I would have recommended acceptance without any hesitation.”
That is a fully human verification, and it is expensive. Four or five researchers spending serious time on one result does not generalize to a pipeline producing dozens of claimed proofs a month.
The three verification methods compared
| Method | What it does | Answers the question | Cost | Limits |
|---|---|---|---|---|
| Human refereeing | Expert reads every step | ”Is this argument valid and does it teach us anything?” | Weeks of expert time per proof | Does not scale; experts are scarce; long proofs risk reader fatigue |
| Formal verification (Lean, Coq) | Machine checks every inference against axioms | ”Is every step logically valid?” | Formalization can take longer than the original proof | Requires translation; a formalized theorem may not match the intended statement |
| Repeated sampling | Run the same prompt many times, count successes | ”How reliably does this model get this right?” | Cheap in compute, tells you nothing about a specific output | A 50% rate does not tell you whether this run is correct |
| Fresh-instance cross-check | New model instances audit the proof | ”Does an independent reader find a flaw?” | Cheap | Models share failure modes; not independent in the statistical sense |
| Spot-checking key lemmas | Expert checks the load-bearing steps only | ”Is the core idea sound?” | Hours instead of weeks | Misses errors in the parts nobody read |
The middle row is where the interesting engineering is. Lean is a proof assistant: you write the argument in a formal language and the software refuses to accept a step that does not follow. If Lean compiles your proof, the logic is correct, full stop.
The catch is the translation. Terence Tao’s January 2025 article in the Notices of the American Mathematical Society argues that interactive theorem provers are changing mathematical practice while raising genuine epistemological questions about what a proof is. Formalizing a research paper has historically taken longer than writing it.
The Liquid Tensor Experiment: proof that formalization can work
The best evidence that this route is viable at research level came before the AI wave, and it is a good story for a teenager.
In December 2020, Peter Scholze, a Fields medalist, publicly challenged the formal-proof community. He and Dustin Clausen had proved a theorem about “liquid vector spaces” that would let functional analysis and complex geometry fit into their condensed mathematics framework. Scholze’s own argument was subtle enough that he was not fully confident in it, so he asked others to formalize and verify it.
The community took it on as the Liquid Tensor Experiment, working in Lean. It was completed on July 14, 2022, about a year and a half after the challenge. Nature and Quanta Magazine both covered it. A proof assistant had made a real contribution at the leading edge of research mathematics by confirming a complicated modern proof.
Two lessons for a kid. First, a Fields medalist asked for his own work to be checked, which tells you something about intellectual honesty at the top of the field. Second, it took eighteen months. That is the timescale problem.
Why 50% success matters more than the proof itself
Here is the number I would put in front of a 14-year-old: OpenAI’s Sébastien Bubeck said the model produced correct solutions in about 50% of trial runs on the same prompt.
Think about what that means operationally. The prompt is identical. The model is identical. Half the time you get a valid proof of a major result; half the time you get something wrong. There is no signal inside the output telling you which one you have.
That is the definition of a tool that requires a competent operator. It is also why Science News noted a real limitation: the data supporting these claims “have not been released or peer-reviewed” and the compute time was not revealed. Melanie Matchett Wood raised a related concern about OpenAI not disclosing failed attempts or incorrect solutions, which is exactly the information you would need to calibrate trust.
In June 2026, more than 1,500 researchers signed the Leiden Declaration calling for guardrails on AI mathematical claims, citing attribution, verifiability, access, and transparency about failure rates. Our piece on what a 50% AI success rate teaches kids about reliability turns this into a dice-and-coins lesson.
How to Teach Your Kid About Verifying a Proof
The transferable skill is checking a chain of reasoning rather than accepting a conclusion. These activities build it.
Ages 5–8: Find the Broken Step
Write out a four-step set of instructions for something they know: making toast, getting dressed, feeding a pet. Insert one impossible step (“put the bread in the freezer until it is warm”). Read it aloud and see if they catch it.
Then flip roles: they write instructions with one broken step and you find it. Writing a broken chain teaches more than finding one, because they have to understand what makes a step valid.
Ages 9–12: The Fake Proof
Show them a classic false proof. The simplest is the one that “proves” 2 = 1: let a = b, so a² = ab, so a² − b² = ab − b², so (a+b)(a−b) = b(a−b), so a + b = b, so 2b = b, so 2 = 1. The error is dividing by (a − b), which is zero.
Have them find the bad step. Most kids will accept the whole chain because every line looks like the last one. That experience, of a plausible chain leading somewhere absurd, is what verification protects against.
Ages 13+: Formalize Something Small
The Natural Number Game is a browser-based Lean tutorial where you prove basic facts about natural numbers from the Peano axioms, starting with things as elementary as 2 + 2 = 4. It is free, open-source under Apache 2.0, and runs at adam.math.hhu.de without installation. It grew out of work by Kevin Buzzard and collaborators at Imperial College London.
Give your teen an hour with it. The experience of the software refusing a step that “obviously” follows is the whole point, and it is the clearest way to understand what Lean does for a 125-page proof. Our guide to proof assistants and how Lean turns math into code covers the tool in more depth.
The question to ask: “Which step in that argument is doing the most work, and how would you check just that one?”
What to actually do at home
Ask for the middle, not the answer
When your child shows you a solved problem, ask about a step in the middle rather than the answer. That is the referee’s move, and it builds the habit of treating a conclusion as contingent on its chain.
Treat “it compiled” as different from “it’s right”
If your kid uses code or a formal tool, distinguish two questions: does it run, and does it do what you meant? A Lean proof that compiles is logically valid, but it might formalize the wrong statement. Same distinction as passing tests versus solving the problem.
Reward finding errors
In most classrooms, finding a mistake in the teacher’s work earns nothing. Make it valuable at home. The scarce skill in the AI era is not producing arguments; it is auditing them.
Use repeated runs deliberately
If your child uses a chatbot for a math problem, have them ask the same question in a fresh conversation and compare. When the answers differ, that is the 50% problem in miniature, and it teaches more than any warning you could give.
What not to do
Do not tell your child that AI proofs cannot be trusted. Some of them are excellent; Gowers said he would have recommended acceptance at the Annals without hesitation. The accurate framing is that they cannot be trusted without checking, which is also true of human proofs, just at a different rate.
What to Watch For Over the Next 3 Months
- Week 4: Whether your child asks “how do you know?” about a claim rather than accepting or rejecting it outright.
- Month 2 red flags: Accepting AI output because it sounds authoritative. The tell is confident fluency with no checkable steps.
- Month 3 self-check: Watch for progress on automated formalization. If translating informal proofs into Lean gets substantially cheaper, the verification bottleneck loosens and the whole landscape shifts.
Frequently Asked Questions
How did mathematicians check the AI’s 125-page proof?
Human refereeing. OpenAI says the proof was checked by a group of external mathematicians who also wrote a companion paper explaining the argument. Noga Alon, Tim Gowers, Arul Shankar, Jacob Tsimerman, and Thomas Bloom all commented publicly. No formal Lean verification of that proof has been announced.
What is Lean and how does it verify a proof?
Lean is an interactive theorem prover. You write a proof in its formal language and the software checks every inference against the axioms, refusing any step that does not follow. If it compiles, the logic is valid. The cost is that translating an informal proof into Lean is substantial work in itself.
Does a 50% success rate mean the proof is only half correct?
No. It means that across repeated runs of the same prompt, roughly half produced a correct proof. The specific proof that was published was checked by humans and found valid. The 50% figure describes the model’s reliability, not that particular output.
Has formal verification ever worked on research-level math?
Yes. The Liquid Tensor Experiment formalized a theorem of Peter Scholze and Dustin Clausen about liquid vector spaces in Lean, completing on July 14, 2022, about eighteen months after Scholze issued the challenge in December 2020.
Can my kid try formal verification?
Yes, with the Natural Number Game, a free browser-based Lean tutorial that starts from the Peano axioms and has you prove elementary facts about natural numbers. It runs at adam.math.hhu.de with no installation and is open source under Apache 2.0.
About the author
Ricky Flores is the founder of HiWave Makers and an electrical engineer with 15+ years of experience building consumer technology at Apple, Samsung, and Texas Instruments. He writes about how kids learn to build, think, and create in a tech-saturated world. Read more at hiwavemakers.com.
Sources
- OpenAI. (2026, May 20). “An OpenAI model has disproved a central conjecture in discrete geometry.” https://openai.com/index/model-disproves-discrete-geometry-conjecture/
- Tao, T. (2025, January). “Machine-Assisted Proof.” Notices of the American Mathematical Society, 72(1), 6–13. https://www.ams.org/notices/202501/rnoti-p6.pdf
- Lean Community. (2022, July 14). “Completion of the Liquid Tensor Experiment.” https://leanprover-community.github.io/blog/posts/lte-final/
- Hulick, K. (2026, June 8). “AI guardrails and the Erdős math problem.” Science News. https://www.sciencenews.org/article/ai-guardrails-erdos-math-problem
- Kakaes, K. (2026, August 3). “Why the legendary Erdős problems are falling to AI.” Quanta Magazine. https://www.quantamagazine.org/why-the-legendary-erdos-problems-are-falling-to-ai-20260803/
- Jiang, E., Liang, X., et al. (with Tao, T.). (2026, July). “From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier.” arXiv:2607.07779. https://arxiv.org/pdf/2607.07779
- Lean Prover Community. “Natural Number Game 4 (NNG4).” https://github.com/leanprover-community/NNG4
