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

  1. Install elan, the Lean version manager (follow the installation instructions on the linked GitHub repository).
  2. 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.


In case of trouble, check out the installation instructions:

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

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 -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 😊

Recommended VS Code extensions