Lean and Mathlib¶

Chapter 1 of the tutorial installs several things with similar names: elan, Lean, lake, Mathlib, a language server and an editor plugin. They are easy to run together, and running them together leads to real confusion, such as expecting Lean to know about the real numbers, or suspecting the editor of checking proofs. In this page we set out what each piece is and, as usefully, what it is not.

The kernel¶

At the bottom sits the kernel, a small program that checks whether a term has the type it claims to have. Since a statement is a type and a proof is a term of that type, this is the same as checking whether a proof proves what it says. Every theorem in these notes, and every one of Mathlib's, ends up in front of the kernel.

The kernel is not a proof search engine and knows nothing about real numbers, games or inequalities. That smallness is the point. Tactics can be large, clever and occasionally wrong, but a mistaken tactic can only produce a term the kernel rejects, never a false theorem. Trusting a Lean proof means trusting the kernel and the axioms reported by #print axioms, and nothing else. Computer scientists call this the de Bruijn criterion, after the designer of the Automath system.

Lean¶

Lean proper is everything else in the bottom two layers: the language, the elaborator that turns what we type into terms, the tactic framework, a compiler, the language server, lake, and a core library of basic types. It is a programming language as much as a proof assistant, and most of it is written in Lean.

Lean is not a computer algebra system. It does not simplify expressions for us or evaluate real numbers, as Computation and the real numbers explains. It is also not an automatic theorem prover, although tactics automate a great deal.

It is easy to overestimate how much of the tutorial depends on Mathlib. We checked each tactic by compiling it in a file with no imports at all, and all but one ship with Lean:

The dependence on Mathlib in these notes is therefore mostly about the real numbers, not about proving.

Mathlib¶

Mathlib is a library, written in Lean and maintained by the Lean community. At the version these notes pin, it runs to 8,311 files and about 2.3 million lines. It contains definitions, such as the real numbers and the standard simplex; theorems, such as le_of_lt; and tactics, such as norm_num, linarith and positivity, which are ordinary Lean programs that happen to live in the library.

Mathlib is not part of Lean, and it is not trusted. Its proofs are checked by the same kernel as ours, which is why a library of this size can be relied on at all. It is also not stable: names are changed and lemmas generalised from month to month. That is why a project pins a Mathlib version in lakefile.toml and a matching compiler in lean-toolchain, and why the two move together. Finally, it is not complete. It has no Brouwer fixed point theorem, for instance, as Nash's existence theorem discusses.

Elan and Lake¶

elan manages toolchains, in the way that pyenv manages Python versions. It reads lean-toolchain and makes sure the lean and lake commands in a project are the matching version. It knows nothing about Mathlib.

lake is the build tool and package manager. It reads lakefile.toml, fetches dependencies such as Mathlib, downloads prebuilt artefacts with lake exe cache get, and compiles a project with lake build. It does not install Lean.

The editor¶

The editor plugin, lean.nvim or the VS Code extension, starts the language server with lake serve and displays what it reports. The infoview is a view onto the server, nothing more. The plugin checks nothing, which is why the same goals appear, character for character, in the output of lake build.

In summary¶

The table below collects the distinctions made on this page.