The story walk
29 ideas, including prerequisites, open the seventeen-chapter mystery. Skip what feels heavy today. Every step pairs a gentle explanation with a pinned Lean excerpt.
Start with step one → All learning pagesReading 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.
Even, odd, and case splits
High school
Splitting numbers into even and odd is the proof’s own first case distinction.
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.
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 Weierstrass standard form
University
Five coefficients fix one standard shape for the curves used here.
Common factors and coprimality
Middle school
Coprime numbers share no positive divisor larger than one.
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.
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.
Coefficients as arithmetic data
University
An expansion expresses the function through a sequence of numbers.
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.
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.
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.
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.
Conductor and level lowering
University
Track problematic primes and use proved conditions to restrict the level.
Contradiction with the same object
High school
Evidence for f ≠ 0 and f = 0 cannot both hold for the same f.
Axioms and proof checking
Proof level
Inspect which foundational assumptions a theorem’s proof uses.