Introduction
Lean is a mathematics proof assistant — a programming language where the "programs" are mathematical proofs, to make sure every step of the proof is justified and verified.
It has gained serious attention in the last few years. For instance, a considerable number of Erdos problems has been solved using Lean and Large Language Models. See here for a commentary of Terence Tao on one of the recently solved problems.
Writing proofs in Lean used to be hard. With the introduction of Aristotle, One can sketch the argument in natural language and translates it into formal code. To showcase its ability, we have formalized some theorems in MAT 3004 – Abstract Algebra I. The traditional lecture notes cen be found here, while the formalized proofs live here.
To make the proof more comprehensible, we create an interactive, line-by-line explanations of the Lean codes via vibe coding. Click below to see what it's doing and why.
Interactive Proof Explanations
Below are some formalized proofs with full interactive walkthroughs. Each page lets you click through the proof line-by-line, with strategy annotations and mathematical context.
To take full advantage of them, you can copy and paste the full formalized proofs on the above link to the online Lean compiler, so that you can trace what is changed before and after adding a new line of proof. Just like pen-and-paper proofs, it usually does one of the following:
(a) setting up an explicit goal to prove the theorem;
(b) adding a new tool in your toolbox;
(c) applying strategies to refine your tools or refine the goal.
Permutation Swap Left
move_swap_left — Shows how composing any transposition with (a b) either cancels
or factors as (a z) · τ where τ fixes a. The key lemma for permutation reduction algorithms.
Permutation Reduction
exists_reduction — When you append a transposition to a list of swaps,
you either reduce the length by 2 (cancellation) or factor out a fixing transposition.
Proved by strong induction + move_swap_left.
Identity is Even Permutation
even_number_of_swaps_of_identity — If a product of transpositions equals the identity,
the list has even length. This makes the sign homomorphism well-defined.
Uses strong induction + contradiction to eliminate the "move" case.
Orbit-Stabilizer Theorem
orbit_stabilizer_theorem — Proves the bijection G/Stab(x) ≅ Orb(x),
establishing |G| = |Orb(x)| · |Stab(x)|. The foundation of Burnside's Lemma and all orbit-counting theory.
Uses quotient induction and the characterization of coset equality.
Preparation of Burnside's Lemma (Sum)
sum_inv_orbit_eq_orbits — Proves that summing 1/|orbit(x)| over every element x equals the number of distinct orbits.
The key counting lemma that makes Burnside's formula work.
Burnside's Lemma
burnside_lemma — The number of orbits equals the average number of fixed points:
|Orbits| · |G| = Σ |Fix(g)|. Proved by double counting, orbit-stabilizer, and the summation lemma.
A cornerstone of enumerative combinatorics.
First Isomorphism Theorem
firstIso — For any group homomorphism f: G -> H, define a homomorphism G/ker(f) -> im(f),
and show that it is an isomorphism.