PIP
“I found lots of correct quilt squares. Surely that finishes the quilt?”
One ambitious quiltStory → proofLoose quilt squares are input pieces. Patching data also specifies how their joins must fit.
Pieces and compatibilityAlgebra.PatchingDatumA 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
Recognize the key challenge in patching: compatible local data must produce one coherent object.
- Nonempty
- The type has at least one inhabitant.
- Subsingleton
- Any two elements of the type are equal.
Original source ↗ · L3779–3789Pinned revision aa2d8b3
theorem solution
{𝒪 : Type} [CommRing 𝒪] [IsDomain 𝒪] [IsDiscreteValuationRing 𝒪]
[IsAdicComplete (IsLocalRing.maximalIdeal 𝒪) 𝒪] [Finite (IsLocalRing.ResidueField 𝒪)]
{ℓ r : ℕ} (hℓ : (ℓ : 𝒪) ∈ IsLocalRing.maximalIdeal 𝒪)
{R : Type} [CommRing R] [Algebra 𝒪 R] {M : Type} [AddCommGroup M] [Module R M]
(P : Algebra.PatchingDatum 𝒪 ℓ r R M) :
Nonempty (Algebra.PatchingLevel 𝒪 r R M ⊥) := by
rcases subsingleton_or_nontrivial M with hM | hM
· exact ⟨FrobDictPC.Limit.trivialLevel P⟩
· haveI : Fact ((ℓ : 𝒪) ∈ IsLocalRing.maximalIdeal 𝒪) := ⟨hℓ⟩
exact ⟨FrobDictPC.Limit.patchedLevel P⟩
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 result is Nonempty (Algebra.PatchingLevel 𝒪 r R M ⊥). rcases subsingleton_or_nontrivial M makes the case split. The trivial branch wraps trivialLevel P; the nontrivial branch installs Fact hℓ and wraps patchedLevel P. Thousands of preceding lines implement the construction invoked by that final application.
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 13/17 · Lean
Pip’s impossible quilt
A thousand local pieces. One pigeon volunteering to glue them randomly.
How we got here
The two workshops supplied objects and a map between them. Patching must also make the pieces compatible. Matching individual pieces is not enough unless the relations between them agree.
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.
- Addition and multiplication togetherA shared set of rules for two operations describes many different number worlds.
- Deformation ringsOrganize all permitted lifts through the maps from one algebraic object.
- Hecke algebrasCollect certain operators on cusp forms and the arithmetic they encode.
- R = T: matching the two workshopsOne surjective map ties the ring built from lifts to the ring built from Hecke operators.
- PatchingCompatible pieces must produce one object satisfying all the required relationships.
MIKA
“We must also match the seams. The input specifies how the pieces are required to fit.”
Edges matterStory → proofAligning the seams prepares one compatible object. Nonempty asks for a witness satisfying the patching-level requirements.
The destination is existenceNonempty (Algebra.PatchingLevelPIP
“An almost empty quilt? Finally, a role with little rehearsal.”
A quiet special caseStory → proofThe empty frame represents the subsingleton special case, where the separate trivial-level construction suffices.
The quiet special caseFrobDictPC.Limit.trivialLevelMIKA
“For the other case, the earlier construction supplies the fitted object. That is where the hard work lives.”
A coherent constructionStory → proofThe sewn bridge is the witness supplied by patchedLevel in the other case. Loose pieces or random glue are not enough.
The assembled bridgeFrobDictPC.Limit.patchedLevelThe idea behind the story
The result is Nonempty (Algebra.PatchingLevel 𝒪 r R M ⊥). rcases subsingleton_or_nontrivial M makes the case split. The trivial branch wraps trivialLevel P; the nontrivial branch installs Fact hℓ and wraps patchedLevel P. Thousands of preceding lines implement the construction invoked by that final application.
What closes the nontrivial branch?
- A witness built by patchedLevel P.
- A finite search over all curves.
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…