The room with no room
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.
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.
Prime numbers
Middle school
A prime is at least two and has no positive divisors except one and itself.
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.
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.
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.
Conductor and level lowering
University
Track problematic primes and use proved conditions to restrict the level.
Cusp forms
University
A modular form with an additional zero-limit condition at every cusp.
Contradiction with the same object
High school
Evidence for f ≠ 0 and f = 0 cannot both hold for the same f.
A room with no guest
Proof level
One theorem proves that every cusp form in one weight-and-level space is zero.