<style>button,.story-clue{pointer-events:none}button{opacity:.55}.story-clue{pointer-events:auto}.panel-select{opacity:1}#app-status{display:none}</style>
A 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 today

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 mathematics

Begin 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.

Why the curve’s arithmetic cannot split the wrong way.

Choose your depthStart with the intuition.
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 what “irreducible” contributes: no proper nonzero subspace survives all the symmetries.

Symmetry
An allowed transformation that preserves the mathematical structure.
Stable subspace
A linear part kept inside itself by every allowed symmetry.
Where the metaphor ends

An uncuttable sphere is only a memory aid. Irreducibility is a statement about a Galois action on p-torsion, not about the physical shape of a curve.

</>S_FreyPackage_Mazur_Frey.lean
Original source ↗ · L77–91Pinned revision aa2d8b3
private theorem mazurM3asmB_of_no_cofixed (P : FreyPackage) :
GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p := by
by_contra hred
have hN : HasGaloisStableCofixedLine (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p :=
rcases mazurM3asmB_exponent_trichotomy P.p P.pp P.hp5 with hsmall | h11 | h17
· exact FreyPackage.frey_no_cofixed_small P hsmall hN
theorem solution (P : FreyPackage) :
GaloisRepIsIrreducible (K := AlgebraicClosure ℚ) ℚ P.freyCurve P.p := by
rcases em ((P.a : ZMod 8) = 3) with h8 | _
· exact mazurM3asmB_of_no_cofixed P

👩🏻‍🎨 Mika · Source reading guide

The claim: this knot of symmetry has no loose strand — no straight line of threads that every shuffle leaves alone. Assuming the strand exists is the wrong-but-useful move. The exits are sealed one by one: the small-prime door, the large-prime door, and finally the no-stable-line argument, so reducibility destroys itself.

Annotated original · not a live Lean state

Point 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 & attribution
Chapter 6/17 · Story

The scissors incident

Pip proposes cutting the problem in half. The symmetries object.

How we got here

The Frey package gave us a curve. We now inspect a representation attached to it. “Irreducible” concerns invariant subspaces of that representation, not whether the drawn curve can be cut with scissors.

These links explain the reading route. A story analogy is not a proof of this theorem.

Take it to the tea salon
PIP
“Snip, snip! Surely this knot splits into a strand plus the rest. Assume it — just for the argument.”
A bold proposal

Story → proofPip’s scissors propose a split. The proof temporarily assumes reducibility to derive a contradiction.

Assume the forbidden splitby_contra hred
MIKA
“The stray strand would be a Galois-stable line: every symmetry of the number world leaves it exactly where it hangs.”
A forbidden line

Story → proofA strand that stayed on its own would be a Galois-stable line. The connected drawing illustrates its role, not its definition.

The forbidden stable lineHasGaloisStableCofixedLine

The idea behind the story

The claim: this knot of symmetry has no loose strand — no straight line of threads that every shuffle leaves alone. Assuming the strand exists is the wrong-but-useful move. The exits are sealed one by one: the small-prime door, the large-prime door, and finally the no-stable-line argument, so reducibility destroys itself.

Does irreducible mean the drawn curve cannot be cut with scissors?

  • Yes, it is a geometric cutting rule.
  • No, it concerns stable linear subspaces under symmetries.

The story and source are readable here. Enable JavaScript to edit proofs, try quizzes, and explore the interactive map.

Some small primes have already been defeated by older methods. Their case files are surprisingly useful.

Read. Try. Make it click.

  1. Read the manga and choose Story, Math, or Lean depth.
  2. Open the proof playground. Edit the tactics and watch the goals change.
  3. Select a state, term, or hint. Wrong turns are part of the story.

The playground checks a small propositional language. FLT excerpts are editable reading material, not live-checked Lean proofs. The complete FLT build remains an upstream verification report.

I’m lost · Help

Mika’s help desk

The scissors incident

One thing at a time

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.

In simpler words

You do not need to know Lean, symbols or university mathematics to begin. Definitions come first in the small stories.

A small clue

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 →