Lean 4

Lean 4 is a program in which mathematics is written down in a way that a computer can check. You type a proof in a very strict, fixed language. Every step must follow from previously established rules. The program then automatically checks whether every single step was actually permitted. If a justification is missing or doesn’t fit, Lean 4 reports an error and the proof is not considered complete. Such programs are called proof assistants: they don’t prove anything on their own, they check what a human or a machine presents to them. The 4 simply stands for the fourth major version, which has been the standard one for several years now.

Why a proof checker suddenly became interesting for AI

Language models, i.e. AI that continues texts, have a well-known problem: they sound convincing even when they’re wrong. This is especially noticeable with mathematics. A calculation can look clean and still contain a flaw in reasoning at some point. A human needs time to find it. Lean 4 finds it in seconds.

This creates something that is rare in AI research: a verdict with no gray area. A proof either passes the check or it doesn’t. Exactly this kind of clear signal is needed when you want to improve a model through trial and error. The model generates thousands of proof attempts, Lean 4 filters out the wrong ones, and training continues with the ones that passed.

For mathematics itself, Lean 4 matters for a different reason. Modern proofs are sometimes hundreds of pages long, and only a handful of experts understand them completely. Formulated in Lean 4, anyone can have the correctness verified without having to think through the proof themselves. Several well-known theorems have been secured this way.

From proof idea to checked code

The foundation is a kind of building-block system. First, a few basic assumptions and rules are laid down, from which everything else is assembled. Every new statement must be traceable back to this foundation without any gaps. The core of Lean 4 that performs this check is deliberately kept small. The less code does the checking, the fewer places there are where errors could hide even within the checker itself.

To keep this practically usable, there are helper commands, so-called tactics. Instead of typing every single step, you write, for instance, a command that transforms an equation on its own. Much of the work is also not proven anew but taken from a huge shared library. This library is called Mathlib and by now contains well over a million lines of checked mathematics, written by volunteers from all over the world.

A common misconception: that Lean 4 is a calculation program like a calculator or a formula software. That’s not the case. Lean 4 doesn’t compute numbers, it checks justifications. And it doesn’t find proofs on its own. Anyone who doesn’t have the idea won’t get anywhere with Lean 4 either.

Lean 4 in research, headlines, and toolkits

You rarely encounter Lean 4 directly in everyday life, but often in AI news. When a lab announces that its model solved problems from a mathematics olympiad, a proof assistant is frequently behind it. The problems are translated into Lean 4, the model searches for a proof, and the check decides on success. This makes it possible to prove results instead of merely claiming them.

A second field is software where errors are costly or dangerous. Related tools are used to formally verify, for example, control software or encryption code for correctness. Lean 4 is not just a proof language in this context but also a programming language. So you can write programs in it and prove properties about them.

Anyone wanting to look into it themselves will find a low barrier to entry. Lean 4 is free, runs in the browser, and is used in introductory courses at universities. There’s even a learning game in which you prove the rules for numbers yourself from scratch. Still, the effort involved is considerable: a proof that a human might sketch in three lines often takes half a page in Lean 4. Narrowing exactly this gap is currently an important goal of research.