Descente Infinie
Your phone rechecks the proof
Free · In‑App Purchases · Designed for iPad. Not verified for macOS.
Fermat's Last Theorem for n = 4, and the kernel that checks it. 8,004 declarations rechecked on your phone in about two seconds. No account, no network, no data.
A proof is only worth what its checking is worth.
In 1995 Andrew Wiles proved Fermat's Last Theorem. In 2026 that proof was written out in full, in a language a machine can check — more than a million named definitions and theorems. Why believe a million lines a machine wrote?
Because a kernel checks the term, and the kernel does not know where the term came from. This app ships that kernel. Not a picture of one, not a green checkmark: the checker itself, running in your hand, on a proof exported from the real thing.
MAKE THE MOVES
Start with something you can hold in your head: n + 0 = n. Tap moves, and the app assembles a real proof term and hands it to the kernel, which accepts it or refuses it. Then try 0 + n = n. The same move is refused — and the reason is not a lesson written into the app, it is how addition is defined. Four rungs, and the last one is proved with the terms you built on the ones below it.
GO DOWN
Fermat's Last Theorem for n = 4 rests on 8,004 named definitions and theorems. Press the button and your device rechecks them, live, with the names streaming past — about two and a half seconds on an iPhone 12 Pro Max. Then walk down through the proof. Every step is a real declaration with its real statement, and every path ends somewhere: at a definition, or at an axiom.
BREAK IT
Why believe the checker? Because you can break it. Seven switches, one for each rule the kernel is allowed to use. Turn one off, run the same proof again, and read the exact count of what stops being checkable. Nothing is simulated; the failures are real failures.
WHAT IT DOES NOT CLAIM
Of those 8,004 declarations, 7,000 are type-checked here and 1,004 — the inductive types, their recursors, and the axioms — are taken as given. The app says which is which, on the screen, every time. It never claims to have checked something it trusted.
FREE, AND WHAT THE PURCHASE ADDS
Fermat's Last Theorem for n = 4 is free, in full. Every mechanic works on it: the moves, the descent, breaking a rule. One purchase adds four more theorems for the kernel to chew on — Euclid on the infinitude of primes, Bézout's identity, Cantor's diagonal argument, and the irrationality of the square root of two, which turns out to be the heaviest of them all. The files are already on your device.
PRIVACY
No account. No network code of any kind. Nothing is collected, because there is nothing to send. It works with the phone in aeroplane mode, in a tunnel, forever.
Built on proofs from the Lean theorem prover and its mathematical library, Mathlib, both under the Apache License 2.0. The kernel in this app is an independent reimplementation and speaks for nobody but itself.
Ratings & Reviews
- This app hasn’t received enough ratings or reviews to display an overview.
The developer, Sungjun Kim, indicated that the app’s privacy practices may include handling of data as described below. For more information, see the developer’s privacy policy .
Data Not Collected
The developer does not collect any data from this app.
Accessibility
The developer has not yet indicated which accessibility features this app supports. Learn More
Information
- Seller
- Sungjun Kim
- Size
- 85.8 MB
- Category
- Education
- Compatibility
Requires iOS 17.0 or later.
- iPhone
Requires iOS 17.0 or later. - iPad
Requires iPadOS 17.0 or later. - Mac
Requires macOS 14.0 or later and a Mac with Apple M1 chip or later.
- iPhone
- Languages
- English
- Age Rating
4+
- 4+
- In-App Purchases
Yes
- The shelf $4.99
- Copyright
- © Sungjun Kim