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 · StoryOriginal 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.
- Compatibility
- Shared parts of different pieces agree.
- Coherent object
- One object satisfying the required relationships all at once.
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
Each piece may satisfy its own rules, but the pieces must also agree where they meet. The input records the pieces and their constraints. A developed construction then supplies one object with all those relationships. This is called patching and supports the deeper lifting machinery.
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 · Story
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
Each piece may satisfy its own rules, but the pieces must also agree where they meet. The input records the pieces and their constraints. A developed construction then supplies one object with all those relationships. This is called patching and supports the deeper lifting machinery.
Is a pile of individually correct puzzle pieces already a complete puzzle?
- No. Their joins and overall compatibility still matter.
- Yes. Glue proves compatibility.
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…