Material für das Seminar "Du beweist noch händisch?!" bei der Sommeruniversität 2024 des Studienwerks Villigst

• The best way: Install lean on your computer
• The fast way: Try lean online

If you are new to Lean/mathlib, a fun way to begin is by playing the the natural number game!

In order to start with the files in this repo, you install lean on your computer (see link above) you clone this repo and run

lake exe cache get
lake build
code .

The last step only opens vscode in case you want to use that.

Docs, Tutorials, search engines

• mathlib4 documentation
• Mathematics in Lean tutorial
• Moogle: Semantic search over mathlib4
• Loogle searches of Lean and Mathlib definitions and theorems.
• abbreviations.json for a list of symbols one can get by typing \ in vscode.

Example projects:

• The Polynomial Freiman-Ruzsa Conjecture blueprint
• Sphere eversion blueprint
• Prime number theorem, blueprint
• 78/100 theorems
• Your next project here!