What is a mathematical proof and how can we represent it? This question was the starting point for the HEGL Illustrating Mathematics Seminar in the Winter Semester 2024-2025, during which we focused on logic and algebra from the constructive point of view, and studied how we can use formal proofs and computer programs to create mathematical games. In this presentation, we will summarise our work and give an introduction to the Lean game that we created. Come around and let us play it together, there will be coffee and cake afterwards!