Follow the story. Try a proof. Let curiosity choose how deep you go.
Walk in through the manga: seventeen chapters, sixty-four pocket pebbles, zero required formulas. The Lean source stays behind glass until you ask for it.
Straight to the mathematicsBegin at the proof map — thousands of named theorems — then climb the full ladder from clock inverses to R = T. The story keeps telling itself beside you; it will keep you honest.
Made for company: one reader who loves math and one who does not — one sofa. Whatever each of you finds carries over to the tea salon.
Seventeen chapters, one extraordinary argument. One small discovery is enough for today.
Pip’s rule: mistakes are clues. Every chapter is open, and every question allows another try.
Powers, smaller problems, and a suspicious parcel.
Search the local catalogue in English or Japanese. Major landmarks have Japanese titles. Open the full original proof on GitHub for the complete context.
The obtain statement uses Int.exists_gcd_one'. Rewriting with mul_pow exposes a common pth-power factor. Int.pow_dvd_pow_iff supplies c′; the final mul_left_cancel₀ needs a proof that the cancelled power is nonzero. This excerpt handles coprimality, not the later parity and mod-four normalization.
Annotated original · not a live Lean statePoint to a story clue or a highlighted term to connect the two.
Try this logical move →Source: anthropics/fermats-last-theorem @ aa2d8b3. Upstream reports verification; this reader has not independently rebuilt the project. Manga explanations are not formal proofs.
Source license & attributionPip packed three umbrellas. The equation packed a common factor.
We have narrowed the exponents. Now we simplify the hypothetical numbers without losing the equation. Recall the scale: an operation is useful only when we track what it preserves. Here we must also track common factors.
These links explain the reading route. A story analogy is not a proof of this theorem.
Already familiar? Keep reading. Otherwise, open a word or follow the prerequisites from the beginning.
Story → proofThe shared ribbons stand for a common factor. The target is a counterexample with gcd one, without that shared baggage.
Remove shared baggageInt.gcd a b = 1Story → proofRemoving ribbons must preserve the contents. The divisibility theorem justifies factoring c as well as a and b.
Justify divisionInt.pow_dvd_pow_iffStory → proofThrowing away a whole bag would lose the evidence. The nonzero lemma ensures the smaller number is still nonzero.
Keep the nonzero evidenceright_ne_zero_of_mul hcStory → proofClosing the lighter suitcase means the equation survives cancellation. The common factor must be nonzero to cancel it.
Cancel with evidencemul_left_cancel₀The obtain statement uses Int.exists_gcd_one'. Rewriting with mul_pow exposes a common pth-power factor. Int.pow_dvd_pow_iff supplies c′; the final mul_left_cancel₀ needs a proof that the cancelled power is nonzero. This excerpt handles coprimality, not the later parity and mod-four normalization.
The story and source are readable here. Enable JavaScript to edit proofs, try quizzes, and explore the interactive map.
Short scenes. Real logical goals. A pigeon who is very invested in your success.
Opening the casebook…
The suitcase diet
Start with the cake-scale story. You only need to read one small piece at a time. If you are in the Fermat story, start with Story depth, then the words listed before the chapter.
You do not need to know Lean, symbols or university mathematics to begin. Definitions come first in the small stories.
Look at the small example before the general formula. Ask what changed and what stayed the same.
Close this panel to return to the exact place you were reading. These are prepared hints for this page.
Start with the first small story →