Logic, algebra and proof visualisation

HEGL Illustrating Mathematics Seminar, WS 2025/26
Florent Schaffhauser, Heidelberg University

Goal of the seminar

  • In this seminar, we explore ways to represent mathematical objects, statements, and proofs.

  • To achieve this, we will learn bout two topics:

    1. Constructive algebra, as exposed in the textbook by Mines, Richman and Ruitenburg.
    2. The programming language Lean, which can be used as a proof assistant to formalise mathematical statements and their proofs.

  • To understand how these two topics interact, we will learn about type theory and (intuitionnistic) logic. It is not required to know anything about this before enroling in the seminar.

Visualisation

  • Last year in this seminar, we created a prototype for the Heidelberg Lean Game, which you can still play online today!

  • The result we chose for the game was the following:

    Let be a domain and let be a prime element in . Then is irreducible.

Schedule and evaluation

  • This seminar is organised in two parts:
    1. Mathematical talks.
    2. Project work.
  • In the second part, we will work as a team, using the resources from HEGL, to create visual artifacts of our work in the first part.
  • One option is to expand the game, but we also want to add a new creative component!
  • You will receive two grades: one for the talk and one for the project work and final presentation. Your final grade will be the average of these two.

Preliminary list of topics for the talks

Date Topic Reference
20.10 Sets and logic I.2, I.3
27.10 Matrices, vector spaces, determinants II.6, II.7
03.11 Polynomials II.5, II.8
10.11 UFDs and Bézout domains IV.1, IV.2
17.11 Divisibility in polynomial rings IV.3, IV.4
24.11 Finitely presented modules II.2, V.2

You should choose a topic soon!

Lean tutorial

def fact : Nat → Nat
| 0     =>  1 
| k + 1 => (k + 1) * fact k

#eval  fact 5  
  -- 120

theorem fact_succ (n : Nat) : fact (n + 1) = (n + 1) * fact n := 
  rfl
  • In December, we will give you an introduction to Lean.
  • We will then use what we learn to add new levels to the game and create tutorial videos.

Can we make formal mathematics more fun to watch?

Propositions-as-types

  • Here is a video about Lean that we can use for inspiration!
  • Do you think you can come up with something better than this? 😅

Where we go from here

  • You can find these slides on the seminar webpage (linked from Müsli).
  • Let us know on Zulip (either in the seminar channel or via DM) which talk you would like to give. The above QR code contains the invitation link.
  • You have until Monday, October 20th at 2 PM to decide! 😊