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

Powers, smaller problems, and a suspicious parcel.

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

See how the smallest odd prime was defeated centuries before the modern machinery — and how the modern proof simply borrows that victory.

Case of three
The smallest odd exponent, dispatched separately from the parcel machinery.
Earlier victory
A theorem for a small exponent, proved long ago and still valid today.
Where the metaphor ends

The pinned excerpt is the modern seam: an import line carries Euler’s proved descent into today’s argument. Descent is a real mathematical argument, not merely a story.

</>S_FLT_fermatLastTheorem.lean
Original source ↗ · L130–139Pinned revision aa2d8b3
theorem solution : FermatLastTheorem := by
apply FermatLastTheorem.of_odd_primes
intro p pp p_odd
by_cases hp5 : 5 ≤ p
· have hp2 := pp.two_le
interval_cases p
· exact absurd p_odd (by decide)
· exact fermatLastTheoremThree
· exact absurd pp (by decide)

👩🏻‍🎨 Mika · Source reading guide

Before the parcel machinery, the smallest odd prime is defeated by a centuries-old descent: any solution would create a strictly smaller one, and that cannot go on forever. The pinned lines show the modern seam where the old victory is simply imported. Read cubes, coprimality, and contradiction first; the folder metaphor is a memory aid.

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 2/17 · Story

The case of three

The one small exponent that earned its own detective folder.

How we got here

The first chapter stated a claim for every exponent ≥ 3. This chapter handles n = 3 separately. Like the stair story, one case and a rule for other cases have different jobs; this one case alone is not the whole theorem.

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

Take it to the tea salon
PIP
“The bounded list is tiny: just three and four survive the narrowing.”
A very short list

Story → proofinterval_cases enumerates candidates inside proved bounds: a finite check, not a search.

Bounded enumerationinterval_cases p

The idea behind the story

Before the parcel machinery, the smallest odd prime is defeated by a centuries-old descent: any solution would create a strictly smaller one, and that cannot go on forever. The pinned lines show the modern seam where the old victory is simply imported. Read cubes, coprimality, and contradiction first; the folder metaphor is a memory aid.

Why does exponent three keep its own folder?

  • The parcel machinery demands five or more.
  • Because three is the largest prime.

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

The folder for three closes. The remaining exponents can be filed: composite ones fold down to primes, and every prime gets a suspicious parcel.

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 case of three

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 →