What is Lean theorem prover?

Lean is a proof assistant: software that checks mathematical proofs the way a compiler checks code. You write a statement and a proof in Lean's language, and Lean either accepts every step or points to the one that fails.

How it works

In ordinary math, a proof is a document that human experts read and judge. Errors can hide for years. In Lean, the proof is a program. A small, carefully built core, called the kernel, verifies that each step follows from the rules of logic. If the kernel accepts the proof, the result is correct relative to those rules, with no need to trust the author.

Think of a spell checker, but for logic. It does not tell you your idea is interesting. It tells you the argument has no gaps.

Lean also has a large shared library of already-formalized mathematics, called Mathlib, so new proofs can build on earlier ones instead of starting from scratch.

What it does not check

Lean checks that a proof proves the statement as written in Lean. It cannot check that the statement matches what a human meant. If someone translates a theorem into Lean incorrectly, the proof can be valid and still answer the wrong question. That is why experts review the formal statement, not only the proof, even when the proof is machine-checked.

Why it matters for AI

AI models are fluent but can state false things with confidence, a problem known as hallucination. A proof checked by Lean offers a different guarantee: the checker does not care how convincing the argument sounds. This makes Lean a natural partner for AI math research, because a model can generate many attempts and the checker filters out the wrong ones. It is also a use of formal verification, which is also applied to software and hardware.

It has limits. Formalizing a proof by hand takes enormous effort, and not all mathematics has been translated into Lean yet. AI models are increasingly used to write the formal version too, which raises the question of who checks that translation.

Neighboring ideas

Lean has been used to examine claims about hard problems such as the Exponential Time Hypothesis and P versus NP. It sits alongside other approaches to making AI output trustworthy, including evals for measuring behavior.

Common questions

Is a Lean proof always right? The logic is, given the statement as written. Whether the statement is the one you intended still needs human review. Do you need to be a mathematician to use it? It is also a programming language, so developers use it too, though the learning curve is steep.