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.
If someone gives you a ticket, can you produce a ticket? Pip has prepared a 40-page plan.
theorem promise (P : Prop) : P → P := by
intro ticket
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.
A ticket before it arrives
“I shall present the ticket I confidently expect to receive.”
exact ticket
Mika’s clue
ticket is not in the context yet. intro ticket assumes the premise P; then exact ticket can return that evidence.
intro ticket
exact ticket
Opening the casebook…
I’m lost · Help
Mika’s help desk
A promise kept
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.