Terence Tao writes for mathematicians on Lean's reliability and the role of AI

On 9 October 2026, Terence Tao posted "What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI" on his blog. The title makes the audience clear: professional mathematicians who are eyeing formal verification and AI systems that write proofs. On Hacker News the post collected 53 points and 7 comments. Only a link, with no text, reached our feed, so we do not retell the author's arguments. Below is the context in which a post like this appears, and why it matters.

Why reliability has become a practical question

Lean began as a project by Leonardo de Moura at Microsoft Research in 2013. Today it is a working tool for large collaborative projects. Tao himself took part in formalizing the PFR conjecture in late 2023, and it took about three weeks. In 2024 he coordinated the Equational Theories Project, which had to determine 22 028 942 implications between 4694 identities on magmas. Without automation and formal verification, neither humans nor referees could have handled a volume like that.

At the same time, language models started working in Lean. In July 2024, Google DeepMind's AlphaProof solved four of six IMO problems and scored 28 out of 42 points. It produced its proofs in Lean. Since then, the question of whether you can trust what comes out of such a pipeline has stopped being a matter for the philosophy of mathematics and become part of everyday work.

Where the trust boundary lies

Lean has a small kernel that checks every term of a proof. Tactics, automation, and model-generated code sit outside the kernel. If they make a mistake, the kernel simply rejects the result. That is what makes pairing Lean with AI attractive: a hallucination in a proof gets caught mechanically.

Some places remain where trust has to be assessed separately:

• Theorem statement. The kernel confirms that the statement as written has been proved. Whether it matches the intended one is for a human to decide.
• Definitions. An imprecise definition in a library or a file makes the proved theorem vacuous.
• Axioms. Lean relies on `propext`, `Classical.choice`, and `Quot.sound`. The `#print axioms` command shows which ones are used.
• `sorry`. This is a placeholder in place of a proof. A file containing it compiles, but the theorem is not proved.
• `native_decide`. This tactic adds the compiler to the trusted base, and `Lean.ofReduceBool` appears in the list of axioms.
• Kernel implementation. Independent checkers exist, for example lean4checker and third-party rechecks, which reduce the risk of an error in the kernel itself.

What AI changes

Before models arrived, the main bottleneck was the formalizer's labor. A model removes part of that burden because it produces proof candidates by the hundreds. Kernel checking stays cheap. But a second task moves to the foreground: making sure the formal statement really says what the author meant. The kernel does not do this work, and a model that fits a proof to a statement can find loopholes in the statement itself. A typical example is a statement that holds trivially because of an empty set or a poorly defined division by zero.

The practical conclusion is that auditing shifts from the proof steps to the conditions of the problem. For mathematicians, this is more a change of skill than a loss of control.

How to work with this

If you plan to use Lean or an AI assistant in research, it helps to follow a short routine:

• Write or reread theorem statements yourself, even if a model generated the proof.
• Before publishing, run `#print axioms` and look for `sorry`.
• Check that the Mathlib definitions you use match your understanding. For nonstandard cases, write counterexamples and verification lemmas.
• For critical results, run the file through an independent checking tool.
• Read Tao's original post. We have given context here, but his arguments and recommendations are best taken from the primary source.