Heidelberg Lean Game

HEGL Illustrating Mathematics Seminar
Winter Semester 2024-2025

Florent Schaffhauser
Heidelberg University

What is Lean?

  • Lean is a programming language that can be used as a proof assistant, i.e. to represent mathematical objects and reason about them.
  • To try it out you can:
    • Play the Natural Number Game.
    • Open a codespace in our seminar repo and go to the LeanIntro, BasicTactics and Logic files.
    • Clone/Pull our seminar repo, open a new branch, and install Lean on your machine (follow the instructions in LeanProject/README).
Status update meeting, 18.12.2024

Paperproof

  • In natural deduction theory, statements derived from others via inference rules can be represented by a proof tree.
  • Paperproof is a Lean 4 extension that enables us to visualize this proof tree (and more).
  • In the project, you will be invited to look at the rendering of your programs in Paperproof (documentation available here).
Status update meeting, 18.12.2024

The Lean 4 Game Server

  • The Lean 4 Game Server is hosted by the Heinrich Heine Universität in Düsseldorf.
  • The code to set up such a server and create a game is available on GitHub.
  • Our objective is to make it work in Heidelberg as well!
Status update meeting, 18.12.2024

Schedule

Date Topic
08.01.25 Lemmas and proofs to be included in the game
15.01.25 Structure of the game, technical infrastructure
22.01.25 Implementation
29.01.25 Wrap-up
03.02.25 Final presentation (HEGL Community Seminar)
Status update meeting, 18.12.2024

Tasks

Topic Persons in charge
Mathematical content Alina, Hannah
Lean implementation Adriano, Heide, Jonas
Game infrastructure Felix, Johannes
Blog post Katrin, Sarah, Vincent
Status update meeting, 18.12.2024

Practice File QR Code Lean syntax Natural Number Game QR Code Natural Number Game

Practice File QR Code Basic tactics Practice File QR Code Logic