Lean

Lean is a special programming language. You don’t write apps in it, but mathematical proofs. A proof is a gapless justification that a statement is true — for example, that there are infinitely many prime numbers. Normally, people write such justifications in words and formulas. Another person then has to read and check them. In Lean, you write the proof so rigorously that a program can verify it. If a step is missing, Lean reports an error. Only once everything checks out is the proof considered confirmed. Such programs are called proof assistants.

Why it matters

AI systems that generate text often sound convincing and are nevertheless wrong. This becomes especially apparent with mathematics. A calculation can look clean and still contain a silent reasoning error in step four. A human then has to laboriously check it. This is exactly where Lean is useful.

Lean delivers a hard verdict: correct or not. There is no “almost right.” This makes it possible to automate AI training. A model generates thousands of proof attempts, Lean sorts out the wrong ones, and the successful ones are used for further training. No experts are needed to evaluate every solution by hand. Companies like Google DeepMind and OpenAI have used this to build systems that solve problems at the level of mathematical olympiads.

Beyond AI, mathematicians also use Lean to check their own work. Some modern proofs run hundreds of pages long, and hardly anyone can verify them completely.

How it works

Lean knows a small set of basic rules of logical reasoning. Every proof step must follow from these rules or from statements already proven. Lean’s core, which checks all this, is deliberately kept small. The less code there is, the fewer places there are for errors of its own.

You can imagine it like a very strict board game. There is a starting position, which is the claim. There are allowed moves, which are the rules of logic. The proof is a sequence of moves toward the goal. Lean only checks whether every move complied with the rules. Creativity is supplied by the human or the AI.

So that not everyone has to start from zero, there is Mathlib. This is a collaboratively maintained collection of more than a million already proven statements. Anyone proving something new builds on top of it. The current version of the language is called Lean 4.

Where you encounter the term

In everyday life, practically never — Lean is a tool for research and teaching. In tech news, however, it comes up regularly. Reports about AI systems winning math competitions almost always mention that the solutions were formalized and verified in Lean. That is the point that makes such results credible.

The term also comes up at academic conferences and in discussions about trustworthy AI. The basic idea interests investors and companies: if a machine can automatically verify results, AI can be deployed in areas where mistakes are costly. Similar verification methods are already used for software in airplanes and chips. Caution when searching: in business German, “Lean” also refers to a method for avoiding waste in production. That has nothing to do with the proof assistant.