The secret duet
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.
Functions
High school
A function gives one output for each permitted input.
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.
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.
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.
Weight and level
University
Weight controls the transformation rule; level chooses which transformations are required.
Congruence subgroups of matrices
University
The level names which matrix transformations are kept and which are sent to zero.
The slash action: the precise weight rule
Master’s level
The transformation law is a bundled equation: f ∣[k] γ = f for every allowed γ.
Coefficients as arithmetic data
University
An expansion expresses the function through a sequence of numbers.
Cusp forms
University
A modular form with an additional zero-limit condition at every cusp.
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.
A hypothetical counterexample
High school
Assume a forbidden solution exists, then keep its evidence together.
Curves defined by equations
High school
An equation describes pairs of coordinates satisfying it.
Clock arithmetic
Middle school
Computing inside a fixed finite set of residues is a number world of its own.
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.
Modularity of a curve
University
Find a qualifying form whose coefficients match the curve’s arithmetic data.