Descente Infinie

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.