Submit the bridge as a ticket
“One bridge, delivered intact. That should count as crossing.”
exact bridgeMika’s clue
bridge has type P → Q, while the goal is Q. Give the bridge its P input: bridge ticket has type Q.
exact bridge ticket
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 todayWalk 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 mathematicsBegin 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.
Pip’s rule: mistakes are clues. Every chapter is open, and every question allows another try.
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 edit is preserved in this tab. The manga explains the original, so its source highlights are paused. This site cannot check the full FLT project.
Source and verification details
Source license & attributionLive practice checker
The proof is yours to finish.
Short scenes. Real logical goals. A pigeon who is very invested in your success.
The backstage switchA promise keptThe bridge needs a ticketBoth musicians must arriveOne door is enoughThe impossible guest
theorem cross_bridge (P Q : Prop) (bridge : P → Q) (ticket : P) : Q := by apply bridge 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.
Opening the casebook…