The aim of this page is to give an outline to get introduced to the formalisation of mathematics and coding with the LEAN prover for master's students and early-career mathematicians.
First steps with LEAN
First steps with LEAN
The aim of this page is to give an outline to get introduced to the formalisation of mathematics and coding with the LEAN prover for master's students and early-career mathematicians.
For your first steps in coding with LEAN, it is recommended to start with the LEAN games. The first ever game was the natural number game (developed by Kevin Buzzard and Mohammad Pedramfar), which formalises the basic properties of natural numbers from the Peano axioms. We have also linked the Topology game and the Hilbert axioms game, which were developed by the Barcelona LEAN seminar and Marc Masdeu, respectively.
Different online LEAN games:
To install LEAN on your computer, you first need to install VS Code. Once you have done this, you should follow the instructions of the LEAN community to install the latest version of LEAN (LEAN4) for your operating system. You can find these instructions here.
In this note, it is also very useful to explore all the resources that the LEAN community offers, such as forums or tutorials. Kevin Buzzard also has a webpage named Xena Project where he has very interesting posts and resources.
Once you have installed LEAN4, there is a more extensive tutorial you should try (a book with all the resources). There was a conference, LEAN for the curious mathematicians, where these were solved and recorded. Marc Masdeu also did a similar effort more recently here.
On a more theoretical side, formalising mathematics is not an easy task. There are many accepted lines of reasoning that we do every day as mathematicians that are not formally correct. In this sense, I recommend watching this introductory video by Patrick Massot, where he explains some classical formalisation problems and their solutions, or this presentation I gave some years ago about formalising limits (following Bourbaki's school and some refinements by the LEAN community).
For many years, there has been a collective effort by the LEAN community to formalise as much mathematics as possible in a GitHub repository named mathlib. To search which results have been formalised, it is useful to refer to this library. Moreover, as a way to check how much formalisation has been developed in LEAN4, the community has a list of 1000 theorems that aim to be proven (some of them have already been proven!).
The mathlib has become the base core of how many AI models have learned to formalise and prove abstract mathematical statements. In this new environment, active mathematicians need the basics of LEAN coding to be able to check and understand all these AI formalisations. Some mathematicians have joined resources to further formalise mathematics with AI; in this sense, they have created an analogous repository to the mathlib using only AI formalisation, named TauCeti.