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.
Either door gets you inside. Your key fits Q. Pip is negotiating with the wall.
theorem one_door (P Q : Prop) (key : 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 key argues with the wrong door
“I picked the left door. Could the Q key please reconsider its type?”
left
exact key
Mika’s clue
left chose the P branch, but key proves Q. Restart the choice with right, then provide key. An Or proof needs one matching branch.
right
exact key
Opening the casebook…
I’m lost · Help
Mika’s help desk
One door is enough
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.