Lean (Proof Assistant)

Lean is a program used to write down mathematics in a very strict notation. The computer reads this notation and checks every single step. If a justification is incorrect, Lean reports an error and does not accept the proof. An ordinary proof in an academic text, by contrast, is text for humans: it contains sentences like “it clearly holds” and assumes that readers will fill in the gaps themselves. Lean does not allow anything like that. Everything must be traced back to a small number of basic rules. Programs of this kind are called proof assistants.

Why this matters

Mathematical proofs today are often hundreds of pages long. Even experts can barely grasp them in their entirety anymore. There have been cases where errors in published proofs were only discovered years later. A verified Lean proof largely rules out this kind of uncertainty.

For AI, Lean is interesting for a second reason. Language models — that is, AI systems that continue texts — like to invent nonsense that sounds convincing. In mathematics, this is especially tricky: an incorrect calculation can look very clean. Lean provides a hard verdict here. The proof either goes through or it doesn’t, with no room for negotiation. This makes it possible to automatically measure whether an AI has really calculated correctly.

How it works

In Lean, one first writes down the claim, for instance that there are infinitely many prime numbers. The proof then follows as a sequence of instructions. These instructions are called tactics. A tactic might say, for example: “assume the opposite” or “apply this already proven theorem”.

The comparison with a programming tool fits well. Anyone writing software immediately gets error messages when compiling the program. In the same way, Lean continuously shows what is still open and where a justification is missing. So one works in dialogue with the program, rather than delivering a finished text at the end.

Also important is a large collection called Mathlib. In it, volunteers have spent years formalizing tens of thousands of theorems from school and university mathematics in Lean. Anyone wanting to prove something new builds on this foundation and does not have to start from the basic rules.

Where the term is encountered

In the news, Lean mainly comes up in connection with AI competitions. In mathematical olympiad problems, AI systems compete by submitting their solutions in Lean. Google DeepMind introduced such a system, AlphaProof, which solved olympiad problems at a high level. OpenAI and several Chinese labs also publish models that generate Lean proofs.

In research itself, mathematicians use Lean for large-scale projects. Fields Medal winner Terence Tao has formalized several of his own results using Lean together with many contributors. Such projects run openly online, usually on the platform GitHub.

Lean is also accessible as a learning tool for pupils and students. There are browser games such as the “Natural Number Game,” in which one works through simple proofs step by step. No prior programming knowledge is required for this, though patience certainly is.