<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

Understand exactly what Fermat’s Last Theorem says before chasing its proof.

Power
aⁿ means multiply a by itself n times.
Counterexample
One allowed choice that would make a supposedly impossible equation true.
Where the metaphor ends

The bakery is a metaphor for the equation. Cake sizes do not prove anything about every integer.

</>S_fermat_last_theorem.lean
Original source ↗ · L129–130Pinned revision aa2d8b3
theorem solution (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n :=
FLT.fermatLastTheorem n hn a b c ha.ne' hb.ne' hc.ne'

👩🏻‍🎨 Mika · Source reading guide

A cake order stands for the equation: three towers of heights a ^ n, b ^ n and c ^ n must come out exactly equal. One square-cake order does succeed, because exponent two is outside the theorem range. The job is to show that no order succeeds once the exponent is three or more, with no empty trays and positive heights throughout.

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

The impossible order

Pip orders three whole-number cakes. The bakery has questions.

How we got here

The square story explained a². Here powers become a question: could three positive whole numbers satisfy aⁿ + bⁿ = cⁿ when n ≥ 3? First understand the claim; the contradiction comes later.

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

Take it to the tea salon
PIP
“One impossible cake order, please: three towers with heights satisfying a ^ n + b ^ n = c ^ n.”
A perfectly legal order

Story → proofA cake order stands for numbers satisfying the equation. The successful square order is outside the theorem’s exponent range.

The impossible equationa ^ n + b ^ n ≠ c ^ n
MIKA
“Careful. The square order went through fine — two is outside the range. This rule only bites from three upward.”
One tiny change

Story → proofChanging the cakes to cubes introduces the exponent condition: the same n must be at least three in all three powers.

Exponent at least threehn : 3 ≤ n
PIP
“No empty trays, no zero towers. Mika checks everyone at the door: positive heights only.”
No empty-tray loophole

Story → proofPip’s empty tray is zero. Mika’s refusal is the positivity condition; b and c have matching conditions too.

No empty trayha : 0 < a
MIKA
“The sealed envelope binds every permitted order at once. One signature, and the whole case is closed.”
A very large promise

Story → proofThe case envelope is a promise about every permitted order. The final line invokes the theorem that supports that promise.

The theorem behind the promiseFLT.fermatLastTheorem

The idea behind the story

A cake order stands for the equation: three towers of heights a ^ n, b ^ n and c ^ n must come out exactly equal. One square-cake order does succeed, because exponent two is outside the theorem range. The job is to show that no order succeeds once the exponent is three or more, with no empty trays and positive heights throughout.

Does 3² + 4² = 5² disprove Fermat’s Last Theorem?

  • Yes. It is an equation with powers.
  • No. The theorem requires exponent 3 or more.

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

There are infinitely many exponents. Pip has brought one very small notebook.

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 impossible order

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 →