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

Live practice checker

The proof is yours to finish.

Short scenes. Real logical goals. A pigeon who is very invested in your success.

Both musicians must arrive

A duet needs both musicians. Pip offers two photographs of himself.

theorem duet (P Q : Prop) (singer : P) (pianist : Q) : P ∧ Q := by
sorry

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

Pip’s wrong-turn notebook

These are invented practice attempts, checked here when you try them. They are not the history of the FLT proof.

The singer plays both parts

“Two copies of the singer. Budget-friendly and mathematically suspicious.”

constructor
· exact singer
· exact singer
Mika’s clue

The P goal is already closed. The remaining Q goal needs pianist; singer still proves only P. One completed part does not replace the other.

constructor
· exact singer
· exact pianist

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

Both musicians must arrive

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 →