Installation and Project Setup

You may install Lean to code on VScode by following the official guide.

1. Create an empty project: in VScode command Lean 4: Project: Create Project Using Mathlib. Depending on internet speed, this may take some time, but you can see a log of progress in real time.
2. Open the folder: use VScode File: Open Folder. Explore the files to get a sense of project structure, but only edit the ones in the My_project_name/ folder, as the others are managed automatically.
3. Import Mathlib: you can import the mathematical library by writing import Mathlib as the first line in the Basic.lean file.
4. Lean4 InfoView: when opening .lean files, you can use Lean 4: InfoView: Toggle InfoView to understand the intermediate state of a proof. Placing the cursor in the middle of the proof will show the available information and the necessary steps next. If strange errors appear but the proof is correct, you can press the Restart File button

Formalization projects start with a blueprint, which gets filled progressively. A sketch of the idea can be found on Terence Tao's blog, but a list of exemplars and the installation guide are also available. For reference, an overview of the available theorems.

A complete reference on the Lean 4 language may be found here.

---

Additional References

Complete Projects

• Analytic Number Theory Exponent Database by Terence Tao et al.
• Equational Theories by Terence Tao et al.
• Polynomial Freiman Ruzsa Conjecture by Terence Tao et al.
• Infinity Cosmos by Emily Riehl et al.
• ABC Exceptions by Bhavik Mehta et al.
• Proofs from THE BOOK by Moritz Firsching et al.
• Soundness of FRI by Bolton Bailey et al.
• Sphere Packing in 8 Dimensions by Maryna Viazovska et al.
• Groupoid Model of Homotopy Type Theory by Sina Hazratpour et al.
• Weil's Converse Theorem by Chris Birkbeck et al.
• Dirichlet Nonvanishing by Chris Birkbeck et al.
• Spectral Theorem by Oliver Butterley and Yoh Tanimoto.
• Automata Theory by Stefan Hetzl et al.
• Seymour's Decomposition Theorem by Ivan Sergeyev et al.
• NeuralNetworks by Matteo Cipollina.

Smaller Projects

• Unit Fractions Density Conjecture: git, paper, blueprint
• Liquid Tensor: git, paper, image, blueprint
• Arithmetic Progressions - Almost Periodicity: home, documentation, git
• Brauer Group and Galois Cohomology: paper, code documentation, blueprint
• Brownian Motion: git, documentation, blueprint
• Toric Varieties: home, paper without lean references, blueprint, upstream-ready
• Combinatorial Games: home, git
• Forbidden Matrix Theory: overview, git, blueprint code
• ∞-Cosmoi for Lean: home, blueprint, docs

Related but through a different formalization language: Busy Beaver Challenge.