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.
Lower the level. Empty the room. Close the case.
Search the local catalogue in English or Japanese. Major landmarks have Japanese titles. Open the full original proof on GitHub for the complete context.
Wiles_Frey returns a negation, implemented as fun hirr => … . The let-pattern unpacks ∃ f, f ≠ 0. Since hf : f = 0 → False, applying it to S2_Gamma0_2_eq_zero f produces False. solution supplies Mazur_Frey P to this negation. In the linked lowering implementation, hmod is formally unused: modularRepOfConductorLevel rederives the needed modular information.
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 & attributionA nonzero guest. A room where every guest must be zero.
One branch produced f ≠ 0; the other gives f = 0 in the same space. These cannot both hold. We return to the hypothetical solution in chapter 1 and reject the assumption that it exists.
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 stone surviving the journey is the nonzero form supplied by level lowering in the level-two, weight-two space.
A nonzero guest at level twolevel_lowering_to_two P (frey_isModular P) hirrStory → proofThe empty display box is the theorem that every form in that same space equals zero. Other spaces are not claimed to be empty.
The same form must be zeroModularForm.S2_Gamma0_2_eq_zeroStory → proofThe stone beside the empty box is one and the same f with evidence for f ≠ 0 and f = 0. Applying hf gives the contradiction.
Nonzero meets zerohfStory → proofThe parcel dissolves because the modularity and irreducibility results rule out a Frey package, breaking the route from a counterexample.
The two results contradictFreyPackage.Wiles_Frey P (FreyPackage.Mazur_Frey P)Wiles_Frey returns a negation, implemented as fun hirr => … . The let-pattern unpacks ∃ f, f ≠ 0. Since hf : f = 0 → False, applying it to S2_Gamma0_2_eq_zero f produces False. solution supplies Mazur_Frey P to this negation. In the linked lowering implementation, hmod is formally unused: modularRepOfConductorLevel rederives the needed modular information.
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 room with no room
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 →