Learn the words, one at a time
No background assumed. Each page starts with its prerequisites and a small example, then reads the actual Lean source.
You do not need the whole mountain in one visit. Every page hands you one small theorem you can genuinely keep — sixty-four pebbles by the end. Skip what feels heavy today; come back for it another day, and enjoy the collecting.
Middle school · High school · University · Master’s level · Proof level
Begin here: objects, conditions and conclusions →Before you memorize it, play with it.
Start with middle-school definitions and formulas, a cake shop and a pigeon detective. Skip familiar ideas; follow the question you want answered.
Find your entrance →Two ways around the mountain
Follow the plot with the story walk, using only the words the mystery needs. Or take the proof walk: all sixty-four ideas, in build order.
Reading a Lean statement
High school
Separate the objects, their conditions, and the conclusion.
Powers and positive integers
Middle school
A power repeats multiplication; positive integers start at one.
Prime numbers
Middle school
A prime is at least two and has no positive divisors except one and itself.
Common factors and coprimality
Middle school
Coprime numbers share no positive divisor larger than one.
Even, odd, and case splits
High school
Splitting numbers into even and odd is the proof’s own first case distinction.
A hypothetical counterexample
High school
Assume a forbidden solution exists, then keep its evidence together.
Functions
High school
A function gives one output for each permitted input.
Comparing remainders
Middle school
Two integers can differ while having the same remainder.
Clock arithmetic
Middle school
Computing inside a fixed finite set of residues is a number world of its own.
Squares on the four-clock
Middle school
A whole-number square sits at 0 or 1 on the four-hour clock — never at 2.
Division on a clock
High school
Coprime to the clock size means a true inverse: a · a⁻¹ = 1 on the residue world.
Addition and multiplication together
Middle school
A shared set of rules for two operations describes many different number worlds.
Fractions and the rationals ℚ
High school
Divisions can leave fractions; the rationals ℚ are the number world that contains them.
How big is a signed number?
Middle school
The absolute value |c| keeps only the size: how far the number sits from zero.
Cubes on the mod-nine clock
High school
Every cube lands on 0, 1 or 8 of the nine-residue clock: the first case of the case-of-three story.
A wider net with a unit
University
To descend, first prove more: a³ + b³ = u·c³ with an arbitrary unit u.
Pick the smallest solution
University
Rank the hypothetical solutions by how often λ divides c: one must be smallest.
Three factors in the Eisenstein world
University
A sum of two cubes splits into three factors once cube roots of unity enter.
Contradiction with the same object
High school
Evidence for f ≠ 0 and f = 0 cannot both hold for the same f.
A stairway that must end
University
A gauge that always strictly decreases cannot decrease forever: Fermat’s descent.
The fourth power folds into a square
High school
A fourth power is a square of a square, so the case of four asks one equation lower down.
Right triangles with whole-number sides
High school
A Pythagorean triple: three whole numbers where x² + y² = z² — the 3-4-5 family.
Tidy triangles share no factor
High school
Primitive triples have coprime legs — and a recipe: m² − n² and 2mn.
The dossier equation, packed once
University
Fermat42 names the suspect once: non-zero a, b and a⁴ + b⁴ = c².
Choose the smallest suspect, again
University
Rank Fermat42 solutions by |c|: a smallest badge must exist.
Two right triangles inside every suspect
University
The Pythagorean classification turns a⁴ + b⁴ = c² into chains of smaller squares.
The smaller suspect appears
University
m, r, s all become squares: i² = j⁴ + k⁴ with |i| < |c|. Contradiction.
Curves defined by equations
High school
An equation describes pairs of coordinates satisfying it.
The discriminant, from quadratics to cubics
High school
One formula can certify whether an equation’s curve is clean or singular.
The quantity c₄, from coefficients to a fingerprint
University
A short polynomial in the coefficients that tells how badly the curve breaks.
The curve’s own addition
University
The curve’s points add: the straight line through two chooses their sum.
Torsion points E[ℓ]
University
The points killed by ℓ-fold addition keep the curve’s arithmetic in a finite cage.
The Weierstrass standard form
University
Five coefficients fix one standard shape for the curves used here.
From the equation to a curve
University
A forbidden solution supplies explicit coefficients of a Weierstrass curve.
Symmetry as a transformation
High school
A symmetry rearranges an object while preserving its rules.
Matrices as transformations
High school
A two-by-two table of numbers describes a transformation with its own arithmetic.
Vectors and subspaces
University
Vectors can be added and scaled; a subspace stays closed under those operations.
Galois representations
University
Encode number-preserving symmetries as transformations of vectors.
Irreducibility
University
No nonzero proper subspace is preserved by every allowed symmetry.
Forms and representations together
Master’s level
One statement asks for curve data and form data to agree inside a residue world.
Semistability
University
A condition controlling how a curve behaves when reduced at each prime.
Counting points: the curve’s number at a prime
Master’s level
Reduce the curve modulo a prime and count that finite point set.
The complex plane
University
Use two real coordinates for a complex number; take the points above the real axis.
Modular forms
University
A complex-valued function with precise transformation and smoothness rules.
Weight and level
University
Weight controls the transformation rule; level chooses which transformations are required.
The slash action: the precise weight rule
Master’s level
The transformation law is a bundled equation: f ∣[k] γ = f for every allowed γ.
Congruence subgroups of matrices
University
The level names which matrix transformations are kept and which are sent to zero.
Cusp forms
University
A modular form with an additional zero-limit condition at every cusp.
A room with no guest
Proof level
One theorem proves that every cusp form in one weight-and-level space is zero.
Coefficients as arithmetic data
University
An expansion expresses the function through a sequence of numbers.
Normalized eigenforms
University
The coefficient sequence obeys extra arithmetic rules, with its first coefficient fixed to one.
Modularity of a curve
University
Find a qualifying form whose coefficients match the curve’s arithmetic data.
Residual modularity
University
Match arithmetic data after passing to a residue setting.
Lifting
University
A theorem recovers fuller information from residual information under extra conditions.
Rings with one gate
Master’s level
A local ring keeps a single maximal ideal: everything outside it is invertible.
Rings that cannot grow forever
Master’s level
Every ascending chain of ideals stabilizes: no endless tower inside the ring.
The discrete valuation ring
Master’s level
A local principal-ideal domain that is not a field: one real gate, one ruler element.
Conductor and level lowering
University
Track problematic primes and use proved conditions to restrict the level.
Deformation rings
Master’s level
Organize all permitted lifts through the maps from one algebraic object.
Hecke algebras
Master’s level
Collect certain operators on cusp forms and the arithmetic they encode.
Surjectivity and isomorphisms
University
Surjectivity reaches every target. An isomorphism also preserves structure and has an inverse.
Patching
Master’s level
Compatible pieces must produce one object satisfying all the required relationships.
R = T: matching the two workshops
Master’s level
One surjective map ties the ring built from lifts to the ring built from Hecke operators.
Axioms and proof checking
Proof level
Inspect which foundational assumptions a theorem’s proof uses.