Logic, algebra and proof visualisation

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

Group project

• We are now done with the mathematical part of our seminar Congratulations to all of you on your talks!
• In the second half of the semester, we will work on the group project, until the day of the final presentation, on 26.01.2026.

Objectives

• Here is what remains to be done:

  1. Implement feedback in your slides and let us know (open a PR ).
  2. Create visual artifacts that illustrate our work on constructive algebra.
  3. Write a blog post for the HEGL Blog, telling the story of this semester's seminar: our goal, our achievments, what we learned.
  4. Prepare slides for the final presentation.

Artifact 1 - A cool video tutorial

• The goal is to create a 5-10 minutes video about a theorem we proved in the seminar.
• It will contain some animation, to explain the material and engage the audience.
• Our models are celebrity YouTuber 3Blue1Brown and former Heidelberg postdoctoral research Alexander Thomas.
• Topic: The discrete fundamental theorem of algebra.

Artifact 2 - A new level for the Heidelberg Lean Game

• Last year we created the Heidelberg Lean Game, which is now available online.
• If you want to lear a bit of Lean, we can add one more level this year!
• To get started with Lean, you can check out the following files: Lean syntax and BasicTactics.
• Topic: Sets and logic.

Schedule for the next meetings

Today is 08.12. There are five more weeks of classes until the final presentation.

This means that you should use the sessions of 15.12 and 05.01 for group work !

The resources of the HEGL are available for you, and the HiWis are there to help.

Repartition of tasks