Computer-assisted mathematics 2024
GitHub repository for the seminar on Computer-assisted mathematics
held at the University of Heidelberg during the Summer Semester of 2024.
Set up the repo
Install Lean
- Install elan, the Lean version manager (follow the installation instructions on the linked GitHub repository).
- Install Lean's current stable version using the following command in a terminal window.
elan toolchain install stable
This will download and install Lean on your computer. You can check that Lean has been installed using the following command.
elan toolchain list
As part of this installation, you should have lake (Lean's package manager) installed on your machine. You can check this using the following command.
lake --version
If this does not work, try closing and reopening your terminal window.
Troubleshooting
In case of trouble, check out the installation instructions:
- In the official Lean manual.
- On the leanprover-community website.
Clone the repo
Either clone this repo using GitHub Desktop or, in a terminal window, go to the folder where you would like to clone it and run the following command:
git clone https://github.com/matematiflo/CompAssistedMath2024.git
This repo uses the mathematical libray Mathlib, so you will need to update your Lean version to the one used by Mathlib at the time you are cloning the repo. You can do so by following the instructions below.
Update your Lean version and download the compiled Mathlib files
Go to the folder where you have cloned the repo and run the following commands.
The first one updates the Lean version used in your repo to match Mathlib's current version (the lean-toolchain file will be modified).
curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
The second command updates your Lean installation and Mathlib dependency.
lake update
The final command below is optional: it downloads Mathlib's pre-compiled files, so you do not have to compile them when you need to import them. It is useful to run it periodically (every day or so!).
lake exe cache get
If this does not work, you can always try to open the current repo in a Codespace 😊