How to check an AI proof with Lean: what the kernel guarantees and what it does not

AI systems now attach Lean files to their proofs, and announcements say "formally verified". That is a strong guarantee about something specific: Lean's kernel has checked every step of a proof of a particular formal statement, using particular definitions and axioms. Whether that statement is the theorem you care about is a separate question, and it is where most problems hide. This guide lists what to check, in order of how often it goes wrong.

1. Is the formal statement the theorem?

Read the statement of the main theorem before anything else — not the proof. Compare it, symbol by symbol, with the theorem in words:

• Quantifiers and order. "For every ε there is a k" is not "there is a k for every ε".
• Number types. A statement over ℕ uses truncated subtraction (2 − 3 = 0) and integer division; over ℝ the same formula means something else.
• Ranges and edge cases. A missing n ≥ 1, or a condition that excludes the hard cases, can make the statement easy or vacuous.
• Definitions in the statement. If the file defines its own notion (a "unique game", a "hard instance"), check that the definition is the standard one — a theorem about a custom definition proves nothing about the standard notion.
• Vacuity. A statement with contradictory hypotheses is true and useless. Check that the hypotheses can be satisfied.

For famous problems, a reviewed formal statement often exists already: Google DeepMind's Formal Conjectures repository states hundreds of open problems in Lean. A proof of exactly that statement leaves much less room for doubt than a proof of a statement written by the same system that wrote the proof.

2. No sorry, no shortcuts

sorry closes any goal without proof. Lean warns about it, but a warning is easy to miss in a long build log. Search the files for sorry, admit and native_decide (which trusts compiled code rather than the kernel), and look for implemented_by and extern attributes that swap a definition for unchecked code.

3. Which axioms does the proof use?

Add a line after the main theorem:

#print axioms main_theorem

A normal Mathlib proof uses only propext, Classical.choice and Quot.sound. Anything else is an assumption the proof did not prove: sorryAx means a sorry somewhere in the dependencies, Lean.ofReduceBool means native_decide was used (the compiler, not the kernel, decided something), and a custom axiom declared in the project is a hypothesis in disguise. An axiom stating the hard part of the problem makes everything after it worthless.

4. Build it yourself, with the pinned versions

Clone the project and build it with the Lean and Mathlib versions it pins (lean-toolchain and lake-manifest.json):

lake exe cache get
lake build

A proof that builds only on the author's machine, or only with a modified Mathlib, is not checked. For extra assurance, tools such as lean4checker re-check the compiled declarations with an independent copy of the kernel.

5. Compare against a statement fixed in advance

The cleanest setup separates the two jobs: someone writes and reviews the formal statement first; the proof must then prove exactly that statement, which a script compares before the kernel checks the proof. This removes the temptation — human or machine — to adjust the statement until it becomes provable. It is how Cairn Commons checks Lean proofs: the statement is pinned when a claim is submitted (or taken from a reviewed problem statement), proofs run in a separate public repository, and reviewers are asked specifically whether the pinned statement says what the words say.

A worked checklist

When all five pass, what remains is the question no tool answers: does this statement capture the problem as mathematicians mean it? That is a question for people who know the field — and the place where a careful review on Cairn Commons counts.

See also

• OpenAI's October 2026 math proofs: what is claimed, what is checked
• Erdős problems and AI, 2025–2026
• The Lean 4 documentation and Mathlib.