Lean: a collaborative forum
The idea is simple: to formalize all mathematical knowledge in a free, open-source proof assistant called Lean (****).
Lean is software for checking mathematical proofs. Programs of this kind have been used to prove the four-color theorem (see les Graphes, Bibliothèque Tangente 54, 2015) and Kepler's conjecture on sphere packing (see Tangente 158, 2014). One of the most widely used proof assistants is Coq, developed by Inria.
Lean was developed in C++ at Microsoft Research by Leonardo de Moura in 2013. It is currently used by several prominent figures, including Thomas Hales, who solved Kepler's conjecture.
To this end, users gather on an online forum called Zulip
(****).
As they get started, their first goal is to learn to use the various tools and become familiar with ways of working different from those they are used to. They aim to digitize the undergraduate curriculum. Half the work has already been done. Here, "digitize" does not mean "scan documents", but enter them into Lean in a format the software can understand. The advantage is that Lean checks whether a proposed proof is valid and consistent with the rules of logic and the axioms implemented in the system.
