The suspicious parcel
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.
The Weierstrass standard form
University
Five coefficients fix one standard shape for the curves used here.
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.
From the equation to a curve
University
A forbidden solution supplies explicit coefficients of a Weierstrass curve.
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.
Fractions and the rationals ℚ
High school
Divisions can leave fractions; the rationals ℚ are the number world that contains them.