Story → proofThe passport stands for evidence of semistability. Kazoo enthusiasm cannot replace a required hypothesis.
The semistable passporthW : W.IsSemistableModelA MATHEMATICAL ADVENTURE FOR CURIOUS MINDS
A small why. A big adventure.
Follow the story. Try a proof. Let curiosity choose how deep you go.
No account. No API key. Just curiosity.
Two ways in. One table between them.
I'd rather not fight math todayWalk 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.
Start with “I don’t know yet.”
Seventeen chapters, one extraordinary argument. One small discovery is enough for today.
17 chapters · LeanOriginal source ↗
Pip’s rule: mistakes are clues. Every chapter is open, and every question allows another try.
A question anyone can askCounterexample detectiveThe symmetry mysterySymmetry spotterBuild the unlikely bridgeBridge builderThe impossible finaleProof navigator
Modularity, the 3–5 trick, and compatible pieces.
9The modularity plan6 min10Langlands–Tunnell6 min11The 3–5 trick6 min12Deformations & Hecke6 min13Taylor–Wiles patching6 min
Explore the whole proof29,511 theorems · original statements · dependencies
Search the local catalogue in English or Japanese. Major landmarks have Japanese titles. Open the full original proof on GitHub for the complete context.
Your discovery in this chapter
Understand the plan for proving modularity before exploring the tools that make it work.
- haveI
- Register a local typeclass instance for later inference.
- resolve_left
- Extract B from A ∨ B and ¬A.
Original source ↗ · L165–180Pinned revision aa2d8b3
theorem modularity_of_semistableModel' (W : WeierstrassCurve ℤ) (hΔ : W.Δ ≠ 0)
(hW : W.IsSemistableModel) : (W.map (Int.castRingHom ℚ)).IsModular := by
by_cases h3 : W.ModRepIsIrreducible 3
·
obtain ⟨M₃, hM₃, hres₃, hcube₃, hns₃⟩ :=
isResiduallyModular_three_and_noInertiaFixedTorsion_and_not_cube_dvd_of_isSemistableModel W hΔ hW h3
haveI : NeZero M₃ := ⟨hM₃.ne'⟩
exact isModular_map_of_mlc1
(liftingAtConductor_three_of_level_hns 3 rfl W hΔ hW h3 M₃ hres₃ hns₃ hcube₃)
·
have h5 : W.ModRepIsIrreducible 5 := (modThreeOrFiveIrreducible W hΔ hW).resolve_left h3
obtain ⟨W', hΔ', hW', h3', hcong⟩ := threeFiveSwitchCurve W hΔ hW h5
Your edit is preserved in this tab. The manga explains the original, so its source highlights are paused. This site cannot check the full FLT project.
👩🏻🎨 Mika · Source reading guide
The by_cases h3 splits W.ModRepIsIrreducible 3. In the positive branch obtain unpacks the level and residual conditions; haveI registers NeZero M₃ for theorem application. resolve_left h3 extracts the mod-five alternative in the negative branch. The remaining switch-and-lift argument continues later in the file.
Annotated original · not a live Lean statePoint to a story clue or a highlighted term to connect the two.
Try this logical move →Source and verification details
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 & attributionChapter 9/17 · Lean
Two doors to the concert
The concert has strict entry rules. Pip has brought a kazoo.
How we got here
The duet introduced what modularity means. Now we examine a strategy for establishing it: start with suitable residual information and use a lifting theorem when its hypotheses hold.
These links explain the reading route. A story analogy is not a proof of this theorem.
Start with these ideas
Already familiar? Keep reading. Otherwise, open a word or follow the prerequisites from the beginning.
- Comparing remaindersTwo integers can differ while having the same remainder.
- Clock arithmeticComputing inside a fixed finite set of residues is a number world of its own.
- IrreducibilityNo nonzero proper subspace is preserved by every allowed symmetry.
- SemistabilityA condition controlling how a curve behaves when reduced at each prime.
- Residual modularityMatch arithmetic data after passing to a residue setting.
- LiftingA theorem recovers fuller information from residual information under extra conditions.
MIKA
“Try the prime three first. If its representation cannot split into a stable part, we can use the lifting route.”
First doorStory → proofThe three-dot door is the mod-three irreducibility branch. With its conditions, residual modularity and lifting give entry.
Try the three-doorby_cases h3PIP
“Three is blocked. Can five get us through the other door?”
Second doorStory → proofThe blocked three-door is the failed first condition. resolve_left uses the either-or result to obtain the five-door condition.
The other door must work(modThreeOrFiveIrreducible W hΔ hW).resolve_left h3MIKA
“A theorem supplies a helper curve with the right conditions. The next chapters explain that detour.”
An auxiliary visitorStory → proofThe helper’s passport represents precise properties promised by an existence theorem. It cannot be any replacement curve.
Find a suitable helperthreeFiveSwitchCurveThe idea behind the story
The by_cases h3 splits W.ModRepIsIrreducible 3. In the positive branch obtain unpacks the level and residual conditions; haveI registers NeZero M₃ for theorem application. resolve_left h3 extracts the mod-five alternative in the negative branch. The remaining switch-and-lift argument continues later in the file.
What does by_cases h3 create?
- Branches with h3 and with its negation.
- An arbitrary choice to ignore a difficult case.
The story and source are readable here. Enable JavaScript to edit proofs, try quizzes, and explore the interactive map.
Live practice checker
The proof is yours to finish.
Short scenes. Real logical goals. A pigeon who is very invested in your success.
Opening the casebook…