VS Code is the recommended IDE for working with Lean 4. To install VS Code, follow these steps:
- Visit the official VS Code website.
- Download the latest version of VS Code for your operating system (Windows, macOS, or Linux).
- Follow the installation instructions provided on the website to complete the setup process.
Once the installation is complete, you can proceed with configuring VS Code for Lean 4 development.
To install Lean 4, please follow these instructions:
-
Install the Lean 4 Extension in VS Code:
- Open VS Code.
- Navigate to the Extensions sidebar by clicking on the square icon on the left panel.
- Search for Lean 4 in the search bar and install the
Lean 4extension.
-
Access the Lean 4 Setup Guide:
- Create a new text file by selecting File > New Text File or using the keyboard shortcut (
Ctrl + Non Windows/Linux orCmd + Non macOS). - Click on the
$\forall$ -symbol located in the top right corner of the window. - From the dropdown menu, select Documentation… > Docs: Show Setup Guide.
- Create a new text file by selecting File > New Text File or using the keyboard shortcut (
-
Follow the Instructions in the Setup Guide:
- Carefully read and follow the instructions provided in the Lean 4 setup guide to complete the installation process.
To clone this repository, run the following command:
git clone https://github.com/pitmonticone/LeanInVienna2024.gitFor detailed instructions, please refer to the GitHub documentation on cloning repositories.
After successfully cloning the repository, navigate into the project directory and execute the following command to retrieve the necessary cached dependencies:
cd LeanInVienna2024/
lake exe cache get
| Date | Time | Speaker | Topic |
|---|---|---|---|
| Sep 18 | 09:00 - 10:00 | Markus Himmel | Introduction to Lean |
| 10:30 - 12:00 | Pietro Monticone | Installation and Basics | |
| 13:30 - 14:15 | Tomáš Skřivan | Scientific Computing in Lean | |
| 14:15 - 15:30 | Pietro Monticone | Logic (1/2) | |
| 16:00 - 17:30 | Pietro Monticone | Logic (2/2) | |
| Sep 19 | 9:00 - 09:45 | Moritz Firsching | Beginner's mistakes using Mathlib/Lean |
| 10:15 - 12:15 | Markus Himmel | Sets and Functions | |
| 13:45 - 14:30 | Markus Himmel | Working with Mathlib | |
| 14:30 - 15:45 | Moritz Firsching | Elementary Number Theory (1/2) | |
| 16:15 - 17:30 | Moritz Firsching | Elementary Number Theory (2/2) | |
| Sep 20 | 09:00 - 09:30 | Markus Himmel | Lean Metaprogramming Overview |
| 09:30 - 10:30 | Tomáš Skřivan | Structures (1/2) | |
| 11:00 - 12:15 | Tomáš Skřivan | Structures (2/2) | |
| 13:45 - 14:30 | Pietro Monticone | Getting Started with Blueprint-Driven Formalisation Projects in Lean | |
| 14:30 - 15:45 | Tomáš Skřivan | Differential Calculus (1/2) | |
| 16:15 - 17:30 | Tomáš Skřivan | Differential Calculus (2/2) |
- Lean Package Registry
- Mathlib documentation is a great reference, but you either need to know where to look, or what things are named. To help with naming, you can reference the naming conventions.
- Loogle is useful if you know something about the types appearing in the statement.
- Moogle is useful if you only know the natural language phrasing.
- LeanSearch
- Zulip Channel "Is There Code for X?"