How to turn mathematical proofs into a game

HEGL Illustrating Mathematics Seminar
Winter Semester 2024-2025
Logic, algebra and proof visualisation

Heidelberg University

What is Constructive Algebra?

"The purpose of computing is insight, not numbers" - Richard W. Hamming (1962).

Classical vs. constructive approach.

Constructive Mathematics:

• Focus on computation.
• Deeper understanding through construction.
• Explicit procedures and algorithms.
• Link between abstract mathematics and practical applications.

Structure of the talk

• What was the seminar about?

• Mathematical content.

• Lean implementation.

• The game infrastructure.

• Your turn: Let us play the game!

What was the seminar about?

• Constructive Algebra.

• Our topics:

  • Basic algebraic structures.
  • Rings and modules.
  • Divisibility in discrete domains.
  • Principal ideal domains.

• Proof visualisation: Lean 4.

• Implementing our proofs into our own Lean Game.

An example from our talks

Theorem: Each matrix over a PID is equivalent to a Matrix in Smith Normal Form.

Proof: It suffices to treat the case of a diagonal matrix. Let .

• Bézout's identity: .

• Corner element divides all of the remaining elements.
• Repeat for the size of .

Mathematical content of the game

Monoid

A monoid is a -tuple such that:

• is a set.

• is a function.

• ( is an element of ).

• is a proof that is associative: .

• is a proof that is a neutral element: .

Group

A group is a monoid equipped with a proof that every element in has an inverse element: such that .

Units in a monoid

Let be a monoid.

• The element is invertible if such that .

• The set of units of is formed of all elements where:

  • ,
  • is a proof that ,
  • is a proof that .

The group of units

Theorem. The set of units of a monoid carries a group structure.

Let be a monoid. Then is a group, where:

• where z is a proof that .
• is the function

Cancellation monoid

A monoid is a cancellation monoid if:

• is commutative, meaning that , .
• has left cancellation, meaning that , if then in .

Unit

• Given a monoid , an element is called a unit if there exists such that .

• We say that is not a unit if it can be proved that ( is a unit) .

Definitions

• Divides. In a monoid, for all , we say that ( divides ) if such that .

• Irreducible. In a cancellation monoid, an element is called irreducible if it is not a unit and, whenever . then a is a unit or b is a unit.

• Prime. In a cancellation monoid, an element , is called prime if it is not a unit and, whenever , then or .

Theorem: Prime elements are irreducible

In a cancellation monoid, let be a prime element. Then is irreducible.

Other possible worlds for the game

• Decidable equality implies that denial inequality is a tight apartness.

• Let be a discrete commutative ring. Then every polynomial has a degree.

• In the real numbers it holds: ( is a unit) and ( is a unit) .

Lean implementation

What is Lean?

• Traditional mathematics: Other people will confirm if your proof is correct.

• Problem: Needs time, effort and people who are willing to check your proof.

• Solution: Take your proof and write it in a proof assistant to see if it is correct.

• Lean: Programming language with strong type checking capabilities, making it possibile to use it as a proof assistant.

• Seminar: We formalised the definition of monoids, units, groups as well as prime and irreducible elements.

Some important built-in tactics

• Simplify your life, use simp.

• Sometimes your goal is near, it is exact.

• What do I want to prove? intro your assumptions.

The type of units

structure Monoid where   -- Implementation: 5-tuple ("set", multiplication, 1, associativity, neutral property)
  carrier      : Type
  op           : carrier → carrier → carrier
  neutral_elt  : carrier
  op_assoc     : ∀ a b c : carrier, op (op a b) c = op a (op b c)
  neutral_ppty : ∀ a : carrier, op one a = a ∧ op a one = a

structure InvElts (M : Monoid) : Type 0 where    -- Triple (element, inverse, property of inverse)
  elt   : M.carrier
  inv   : M.carrier
  isInv : M.op elt inv = M.neutral_elt ∧ M.op inv elt = M.neutral_elt

def invMap (M : Monoid) : InvElts M → InvElts M :=    -- sends an element in InvElts to its "inverse"
  fun ⟨x, y, p⟩ ↦ ⟨y, x, by constructor; exact p.2; exact p.1⟩ -- we need to construct  the third term
  -- which is a proof of the proposition `M.op y x = M.neutral_elt  ∧ M.op x y = M.neutral_elt`

Primes and irreducibles

--definition unit
def unit (n : Nat) : Prop :=
  ∃ m : Nat, m * n = 1 ∧ n * m = 1

--definition irreducible
def irred (n : Nat) : Prop :=
  ∀ a b : Nat, n = a * b → unit a ∨ unit b

-- definition prime
def prime (p : Nat) : Prop :=
  (∀ a b : Nat, p ∣ (a * b) → p ∣ a ∨ p ∣ b) ∧ (0 < p)

Prime implies irreducible

Let us look at the code.

The game infrastructure

Your turn: Let us play the game!