nimarasekhFormalization_SoSe25

Teaching Material for Course on Formalization Summer Semester 2025 at Uni Greifswald

Formalization Seminar SoSe 2025 Uni Greifswald

This the course webpage for a seminar on formalization in Lean at the Universität Greifswald in summer semester 2025. The goal is to learn something about formalization of mathematics and how to use the proof assistant Lean.

Some Theoretical Background

Here are some sources about the underlying theoretical aspects:

Here are some sources about various proof assistants:

Some First Steps before the First Steps

Before starting with installations on your computer, you could try some of these games online (however, not required):

Setting Lean Up on your Computer

Participation in the seminar requires several local installations on your own computer.

Please following steps (before starting the steps read the whole instructions once):

  • Follow the steps outlined in the following instructions
  • Note: Part of the installation involves installing Visual Studio Code (where we write Lean code) and git (for version control)
  • Warning: if you are using Windows you might have to deactivate your anti-virus during the installation process!
  • Small Change: In the step Set up Lean 4 project click on Download an existing project (third bullet point). Choose Git repository URL, enter https://github.com/nimarasekh/Formalization-SoSe25 and then select a folder where you want to download this repository, and specify a folder name. Then press Create project folder and wait a few minutes.

  • When you have downloaded the repository a message appears allowing you to open the project folder. To test that everything is working, open the repository and open the file Formalization-SoSe25/Cover.lean. The file should be ready a few seconds later. Try out the CLICK HERE in the file and see if you get the correct responses.

  • A useful (but optional) extension is the VSCode extension Error Lens. If you install this, you will see messages from Lean right in the file where you're typing.

Troubleshooting

Note: To get this repository, you will need to download Lean's mathematical library, which takes about 5 GB of storage space.

It might be tricky to get Lean running on a laptop that is more than 10 years old or on a chromebook, since Lean does use a moderate amount of recourses. You can still run Lean in your browser by using Codespaces or Gitpod, see the the instructions at the bottom of this file.

  • If you get errors such as curl: (35) schannel or uncaught exception: no such file or directory (error code: 2) take a look here.

Update repository

I will update the lectures and exercises as we go along. In order to get the most recent updates you have to pull the changes. There are several options:

  • Open the terminal in VS Code (ctrl+` /cmd+` ) and then write git pull and press enter.
  • Open the Source Control tab in VS Code (third icon in the top-left, or ctrl+shift+G/cmd+shift+G) and then under ⋯ (More actions) you can click Pull to get the latest changes.
  • Note: If you use Source Control you should not press Sync, since that will try to upload your changes to the assignment files to GitHub (you don't have the rights to do this).
  • Occasionally there is an update to the Lean version for the repository, in which case you will be informed. In that case after

We might at some point update the version of Lean for the repository (we will tell you when this happens). In that case it is necessary to get the new Mathlib cache via the following steps.

  • Do not restart a Lean file (which will prompt Lean to rebuild Mathlib on your laptop).
  • If pulling happened via terminal, then still in the terminal run lake exe cache get! (or ~/.elan/bin/lake exe cache get! if lake cannot be found).
  • In the VS Code window ∀ > Project Actions... > Fetch Mathlib Build Cache and wait for the cache to download.
  • After it has finished, you might have to restart the Lean file, and then Lean should be compiling your file in less than a minute.

If this fails, try the following steps:

  • Close VSCode (if it is open)
  • Open terminal on your computer in the LeanCourse24 folder.
  • Run lake exe cache get! (or ~/.elan/bin/lake exe cache get! if lake cannot be found).
  • Wait until the command finishes with downloading and decompressing. If you get an error, run it again.
  • Now you can reopen VSCode and restart the file (if prompted).

Setting Things Up Online

If there are any challenges with the local installation, here are some (temporary) online solutions:

  • There is an online option for experimentation with Lean: Lean Online
  • A more advanced option is to work with the project via GitHub Codespaces:

Open in GitHub Codespaces

  • Another option to work with the project is via Gitpod:

Open in Gitpod

Learning Material

  • The learning material consists of lectures and exercises that can be found in this repository.
  • No other material is mandatory, but recommended material can be found further below.

Additional Learning Material

Here are some interesting books and learning material, that will serve the basis for the lectures here:

Some Other Recommendations

  • It is recommended to make a GitHub account now. It will become mandatory later on for the projects.

Acknowledgement

The style and the content is very much motivated by the work of Floris van Doorn for his course in Winter semester 2024. The course material and exercises are heavily influenced by Mathematics in Lean.