The workshops agree
The prerequisites are included before the words that depend on them. Skip what you already know.
Start with step one → Return to the storyReading 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.
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.
Addition and multiplication together
Middle school
A shared set of rules for two operations describes many different number worlds.
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.
Curves defined by equations
High school
An equation describes pairs of coordinates satisfying it.
The curve’s own addition
University
The curve’s points add: the straight line through two chooses their sum.
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.
Symmetry as a transformation
High school
A symmetry rearranges an object while preserving its rules.
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.
Cusp forms
University
A modular form with an additional zero-limit condition at every cusp.
Coefficients as arithmetic data
University
An expansion expresses the function through a sequence of numbers.
Common factors and coprimality
Middle school
Coprime numbers share no positive divisor larger than one.
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.
Vectors and subspaces
University
Vectors can be added and scaled; a subspace stays closed under those operations.
Torsion points E[ℓ]
University
The points killed by ℓ-fold addition keep the curve’s arithmetic in a finite cage.
Galois representations
University
Encode number-preserving symmetries as transformations of vectors.
Irreducibility
University
No nonzero proper subspace is preserved by every allowed symmetry.
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.
Semistability
University
A condition controlling how a curve behaves when reduced at each prime.
Lifting
University
A theorem recovers fuller information from residual information under extra conditions.
Division on a clock
High school
Coprime to the clock size means a true inverse: a · a⁻¹ = 1 on the residue world.
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.
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.
The discrete valuation ring
Master’s level
A local principal-ideal domain that is not a field: one real gate, one ruler element.
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.