When an AI system announces it has proved a decades-old open problem, the honest answer to “is it true?” is: not yet — not until the argument has survived scrutiny far stricter than reading it and nodding along. Mathematicians check an AI’s claimed proof the same way they check a human’s: by re-deriving every logical step, and increasingly, by feeding the argument into software that checks it line by line against the axioms of mathematics. A claim becomes an accepted theorem only once it survives that process.
Two very different kinds of “proof”
Modern AI systems produce mathematical arguments in two modes that look similar but aren’t. The first is an informal, natural-language proof — the AI writes out reasoning in ordinary mathematical prose, the way a human would in a journal paper. The second is a formal proof, written inside a proof assistant such as Lean, a programming language in which every step must be justified by a rule the computer can check automatically. Google DeepMind’s AlphaProof took the formal route: trained with reinforcement learning to search for Lean proofs, it helped reach silver-medal-level performance at the 2024 International Mathematical Olympiad by formally proving several competition problems inside Lean.
Why “formal” is the trust boundary
The difference between those two modes is the whole trust question. A natural-language proof can read as persuasive and still hide a gap — mathematics has a long history of published proofs that took months, or years, for human referees to find flawed. A formal proof, once it compiles inside a system like Lean, has been mechanically checked against a fixed set of logical rules; there’s no room for a step that merely sounds right, because an unjustified step simply won’t compile. That’s why the strongest form of certainty in mathematics has shifted, for an increasing share of results, from “did enough experts read it carefully” to “did it type-check.” This isn’t new: the 1976 four-color theorem was first proved with a computer checking thousands of cases by hand-written logic, but many mathematicians didn’t fully trust it until it was independently re-verified inside a formal proof assistant in 2005.
AI is straining the verification pipeline
What’s new is the volume. Fields medalist Terence Tao has described a growing “impedance mismatch”: AI can now generate candidate proofs far faster than any team of human specialists can read and check them, so the bottleneck in mathematics is shifting from generating ideas to verifying them. Tao has pushed large-scale formalization projects that encode published results in Lean’s community-maintained library, mathlib, which has grown past 200,000 formalized theorems, and he has personally used a chatbot as a translator — converting a hand-written proof of a decades-old Erdős problem into more than 1,100 lines of Lean code that a machine could check step by step. That points to where the field is heading: not just AI generating proofs, but AI helping formalize and verify them too, closing the gap it opened.
For a headline claim about an AI proving a famous conjecture, the practical rule of thumb is simple: treat it as provisional until either (a) the argument has been translated into a formal system like Lean and compiles cleanly, or (b) independent domain experts have gone through the natural-language proof line by line and published their assessment. Neither step happens instantly, which is exactly why bold proof claims and confirmed theorems are announced on different timelines.
In the news
A recent example of this pattern working through in real time is our report on OpenAI’s GPT-5.6 Sol Ultra claiming a proof of a 50-year-old math conjecture — the kind of claim that, per the process above, stays provisional until formal or expert verification catches up with it.
FAQ
If a proof compiles in Lean, does that make it automatically true?
It means the argument follows validly from the system’s own axioms and inference rules — which is why proof assistants like Lean are themselves open-source, extensively tested, and open to public scrutiny, so the foundation being checked against is trustworthy too.
Are all AI math claims formally verified?
No. Many headline results are informal, natural-language arguments that still require expert human review, or translation into a formal system, before mathematicians treat them as settled.
Can I try a proof assistant myself?
Yes. Lean is free and has both browser-based and downloadable tools; the community’s getting-started guide is the standard entry point, no math PhD required to explore it.
Has AI produced a genuinely new, formally verified result?
Yes, in bounded settings — AlphaProof’s olympiad-level Lean proofs and mathematician-AI collaborations like Tao’s are real, checked results — though these remain narrower in scope than open research conjectures, where formal verification of AI-generated arguments is still the exception rather than the rule.