Written by Vincent Voß, Katrin Weiß
This Lean Game was created as a group project during a HEGL seminar by Heide Frank, Johannes Kadel, Adriano Messina, Hannah Roth, Jonas Schäfer, Alina Stock, Vincent Voß and Katrin Weiß.
What is a mathematical proof and how can we represent it? To answer this question, we can use a constructive approach, as opposed to a classical one, to turn mathematical proofs into games. Can we use this method to guess how mathematics will be taught at the university level 50 years from now?
This was the driving question for the HEGL Illustrating Mathematics Seminar last semester. We focused on logic and algebra, as well as their proof visualization. The goal was to explore how mathematical objects and proofs can be represented using computer programs. Below, you will find some insights about our seminar, as well as the Lean game which we created.
To begin, here is the question we asked at the beginning of the seminar:
What is Constructive Mathematics?
Classical Mathematics often focuses on describing truths. One example is the Fundamental Theorem of Algebra, which states that every polynomial with complex coefficients has at least one root. A classical proof would start by assuming that a polynomial without a complex root does exist, leading to contradiction. In contrast, Constructive Mathematics requires explicit procedures for finding solutions. A constructive proof of the Fundamental Theorem of Algebra would need to provide a concrete step-by-step algorithm for computing the complex roots of any given polynomial, not just claim their existence. In this case, we cannot just prove the theorem by contradiction, but instead, we have to define several propositions that make up the whole proof. Because of this, Constructive Mathematics is closely linked to computational approaches and links abstract mathematics and practical applications – constructive proofs, therefore, often provide more information. In this blog post, the reader will learn, in more detail, about the construction of these proofs, from the mathematical part up to the implementation into Lean.
The methodologies of Constructive Mathematics can be applied to many different fields. In our seminar, we looked at Constructive Algebra. First, you need to think about how to define sets and logic in this new constructive setting, until you can talk step-by-step about further algebraic structures like rings and modules, or divisibility. Proving a theorem means constructing a proof of it, much like when you introduce a term of a certain type in a programming language. The underlying logical foundations of this approach make functions the primitive object, from which everything else is defined. In the first part of the seminar, the students gave presentations on undergraduate commutative algebra. First, we learned about sets and logic, then about basic algebraic structure. With this basic input, we continued examining rings and modules, as well as divisibility in discrete domains. In the end we discussed invertible elements in a monoid in detail – always focusing on presenting definitions and proofs constructively. You can find our presentations on the seminar website. This constructive approach was somewhat difficult for the class to understand initially, as it differs from other mathematics seminars at Heidelberg University. That’s why we asked:
How can we introduce Constructive Algebra?
Our talks were based on the book by Mines, Richman, and Ruitenburg (1988): A Course in Constructive Algebra as well as an introductory presentation by our instructor, Florent Schaffhauser, on sets and logic.
In order to discuss mathematical concepts, we need to establish rules for constructing elements of a set and identifying or distinguishing elements. Logic must be formally introduced in constructive mathematics, in the same language that is used to introduce mathematical objects.
For example, equality is a relation between the elements of a set \(X\), while inequality can be defined as the negation of equality. A binary relation that fulfills the properties of reflexivity, symmetry, and transitivity, is called an equivalence relation. For a set \(X\), expressions such as \(x = y\) or \((x = y \Rightarrow y = x)\) or \(((x = y) \wedge (y = z))\) are examples of propositions – which does not mean that they are true statements. The main question that remains is whether we can construct a proof for these propositions. Propositions, just like sets, may or may not have elements (called proofs). When we consider equality between two elements in a set, we ask ourselves: Can we construct a proof for \(x = y\)? To answer this question, we need a formal definition of equality. To dive deeper into Constructive Algebra, let us take a look at implications and conjunctions. Assuming that \(P\) and \(Q\) are propositions, what does \(P \Rightarrow Q\) or \(P \wedge Q\) mean? What does it mean to prove the conjunction \(P \wedge Q\)? It is the proposition whose proof consists of pairs \(\langle p, q\rangle\) where \(p\) is a proof of \(P\) and \(q\) is a proof of \(Q\). All steps of the proof are defined constructively, and we need to set up rules to construct and introduce proofs.
Through the presentations on basic algebra, rings and modules, and divisibility in discrete domains and principal ideal domains, we have learned to use constructive definitions step by step for the proofs of theorems and lemmas. For example, the constructive definitions of an (abelian) monoid, a unit and a group, which were formulated for a possible project to show that the set of units of a monoid is a group. In fact, this project was later implemented in Lean and carried out in a guided manner:
Definition of a monoid
Be \(M\) a set and \(\forall a, b, c \in M\):
– “Multiplication”, meaning that, \(\varphi: M\times M \rightarrow M, \varphi(a, b)=ab\).
– Associative law, meaning that, \((ab)c=a(bc)\).
– Identity, meaning that, \(\exists e\in M\) so that: \(ea=ae=a\).
In a “multiplicative monoid”, \(e\) is often denoted by \(1\). In an “additive monoid”, by \(0\).
Abelian monoid
\(\forall a, b\in M\), \(ab=ba\).
Unit
\(a, b, e\in M\):
– b is an inverse of a, meaning that: \(ab=ba=e\).
– We also write \(b=a^{-1}\).
– Then a is a unit, meaning that it is invertible.
Definition of a group
– “Next step” after monoids.
– Every element is a unit.
– \(G=\{a \in M \;|\; a \text{ is invertible}\}\).
Possible project
Show that the set of units of a monoid is a group.
– \(\{a \in M \;|\; a \text{ is invertible}\}\) is a group.
To find out more about how our process worked after our presentations, next we need to answer the question:
What is Lean?
Constructive Algebra and its proofs can be illustrated very well with Lean, a programming language that can be used as a proof assistant. The first version of Lean was published in 2013, while the current version is Lean 4. It has a growing community all over the world.
To use Lean, you need to adopt a new understanding of mathematics, very similar to the ways constructive mathematics differs from classical maths. You need to think about propositions as types and terms as proofs, and use tactics to prove your theorems. The keyword to enter the tactic mode in Lean is “by”. Some helpful tactics to use are rewrite (rw), dsimp, exact, rcases, intro, exists, have. For example, you can use dsimp to unfold your definitions. The tactic mode will tell you when your proof was successful and tell you when something is still missing. To close a goal, you need to use the tactic “exact”. Moreover, Lean is an interactive theorem prover, meaning that it focuses on the verification aspect of proofs. This causes the user to be very precise and justified by all definitions and propositions you give beforehand. Besides tactics, there’s also terms that are already proven in Lean that you can use as tools for your proofs. An example is the term [Nat.mul_assoc] which you can use whenever you want to use the associativity of the natural numbers.
To learn more about Lean and get a more detailed introduction and instructions on how to prove theorems, click here.
Because of the precision necessary for Lean, we had to decide on which mathematical contents we wanted to implement in our game, and how we would be able to do it. We formed multiple focus groups, some students focused on the mathematical content, some on the implementation in Lean and so on. An example of Lean code that we worked on, in order to understand how it works, was to define algebraic structures like monoids. We had to figure out how these definitions worked and how to define elements, operations, and more. Something that caught our attention was that structures like Monoids and Groups are defined as tuples within Lean, which you also need to have in mind and pay attention to when writing your proofs. After making these definitions, you can start to prove things, for example, that multiplication is well defined on a monoid:
-- Proof that multiplication is well-defined
mul := λ x y => ⟨M.mul x.1 y.1, M.mul y.2 x.2, by {
constructor
case left =>
rw [M.mul_assoc]
rw [←M.mul_assoc y.elt _ _]
rw [y.isInv.1]
rw [(M.one_mul x.inv).1]
rw [x.isInv.1]
case right =>
rw [M.mul_assoc]
rw [←M.mul_assoc x.inv _ _]
rw [x.isInv.2]
rw [(M.one_mul y.elt).1]
rw [y.isInv.2]
}This was the first proof on the algebraic structure of a monoid. If you want to see the full Lean code, click here. This way, you can slowly build your algebraic structures and start to define what an inverse or a unit is. After these steps, we had to think about what we wanted to implement in the game, which you will have to discover for yourself.
Besides turning them into a game, the proofs in Lean can also be visualized using a program called “Paperproof”. Here’s an example of the proof that uses case analysis to prove if a prime element p divides a or b, either a or b have to be a unit:
After knowing about the mathematical and infrastructural basics, the last part of our seminar was mainly about creating the game using our proofs in Lean. We want you to enjoy the game, which is why we will explain:
How do you play the game?
A Lean Game server set up by Heinrich-Heine-Universität Düsseldorf already exists, and our goal in the seminar was to create a game of our own here in Heidelberg within the contents and limitations of the seminar. Everybody is invited to try it out and play.
During the seminar, we wrote a complete World and now the infrastructure is in place to write additional Worlds. When you access our game, you will first find an overview and some introductory explanations. The World we chose to implement into our game has the following structure:
World 1: Divisibility
– Level 1: Cancellation in ℕ
– Level 2: Equality Implies Divisibility
– Level 3: Substitution in ℕ
– Level 4: Proving v is a Unit
– Level 5: Case 2: Proving u is a Unit
– Level 6: Prime Implies Irreducible
In this World you will work through a series of levels that explore basic properties of divisibility in the natural numbers. Each level builds on the previous one: Level 1 introduces the cancellation law, Level 2 shows that equality implies divisibility, Level 3 covers a substitution property, Level 4 and Level 5 establish unit properties. In the end, Level 6 brings these concepts together to prove that every prime number is irreducible. That is why it is recommended that you start with Level 1 in World 1 and work your way through the game from there. While solving the levels, the middle of the screen will show the theorem that you want to prove and contain the space for you to type your solutions. You will see explanations and hints on the left-hand side, while on the right, you will see the available tactics, definitions, and terms you can employ to solve the level. We hope that you will have some fun and that our game will give you some deeper understanding of how proofs work.
Is this how mathematics will be taught at universities in 50 years’ time?
Get to know our Heidelberg Lean Game and the advantage of constructive algebra in guided proofs and answer the question yourself!
To take a deeper dive into what we did during the semester, and get another structured overview, see our final presentation, where we tried out our game with members of the HEGL Community within the HEGL Community Seminar on 5th of February 2025. Feedback was great and the potential of our main question was confirmed by the participants.
In the following semesters, the HEGL community will offer more seminars like this one and thus implement and publish more guided proofs to enrich maths studies in this respect.