<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 a proof can cover infinitely many exponents without checking them one by one.

Prime
A whole number greater than 1 whose only positive divisors are 1 and itself.
Reduction
Turn a solution of one problem into a solution of another, so ruling out the second rules out the first.
Where the metaphor ends

Sorting folders represents a proved reduction. It is not permission to discard inconvenient cases.

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

The stack of exponents never ends, so ticking folders one by one can never finish. Instead the proof folds the map: if exponent four falls and every odd prime falls, everything else is covered by them. The drawer for three is already shut, and the big-prime folders travel with the Frey-package crew.

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

Too many suspects

Infinitely many folders. One suspiciously small filing cabinet.

How we got here

After the special exponent 3, we organize the remaining exponents. Rewriting a power as a power of a power lets a hypothetical solution lead to a smaller collection of cases.

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

Take it to the tea salon
PIP
“Case files stacked to the ceiling. Checking them one by one would outlive the paperwork itself.”
An ambitious filing system

Story → proofThe tower of folders is the infinitely many exponents. Finishing an endless checklist cannot establish the goal.

All exponentsFermatLastTheorem
MIKA
“Then fold the map: hold down exponent four and all odd primes — the rest are only copies of those.”
A smaller job, with a proof

Story → proofFolding the map is a reduction: exponent four and odd primes suffice to cover the original claim.

Reduce to odd primesFermatLastTheorem.of_odd_primes
PIP
“The three drawer is already shut, and the by_cases split keeps it away from five and up.”
The small print

Story → proofThe closed drawer is the resolved exponent-three case. The case split separates it from primes at least five.

Separate the small casesby_cases hp5 : 5 ≤ p

The idea behind the story

The stack of exponents never ends, so ticking folders one by one can never finish. Instead the proof folds the map: if exponent four falls and every odd prime falls, everything else is covered by them. The drawer for three is already shut, and the big-prime folders travel with the Frey-package crew.

If a⁶ + b⁶ = c⁶, what regrouping gives exponent 3?

  • (a²)³ + (b²)³ = (c²)³
  • (a+2)³ + (b+2)³ = (c+2)³

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

The remaining counterexample arrives as a parcel. Unfortunately, it has paperwork.

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

Too many suspects

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 →