Dit project presenteert een machine-geverifieerd bewijs van de Laatste Stelling van Fermat in Lean 4, gebaseerd op de wiskundige argumentatie van onder anderen Frey, Ribet en Wiles.
Belangrijkste aspecten van het project:
- Verificatie: Het bewijs is rigoureus gecontroleerd via de Lean-kernel, de
comparator tool en nanoda, een onafhankelijke kernel geschreven in Rust.
- Documentatie: Er is een uitgebreid HTML-archief beschikbaar waarin de route van het bewijs en bijna 30.000 stellingen offline kunnen worden geraadpleegd.
- Technische vereisten: Het zelf verifiëren van het project is zeer hardware-intensief; er wordt melding gemaakt van piekgeheugenbehoeften tot 300 GB RAM voor bepaalde controles.
- Herkomst: De bronnen zijn gegenereerd door AI-agenten die voortbouwen op bestaande open-source Lean-projecten en Mathlib.
Het project is uitgebracht onder de Apache License 2.0 en fungeert als een onderzoeksartifact.
De Laatste Stelling van Fermat in Lean 4
In het bestand PROOF-PATH.md wordt elke stap benoemd samen met de bijbehorende Lean-stelling. De map html/ presenteert het volledige bewijs als webpagina's die offline kunnen worden geraadpleegd.
Let op: Dit is een onderzoeksartifact. Het wordt niet onderhouden en er worden geen bijdragen geaccepteerd.
De stelling
In Theorems/Thmfermatlast_theorem.lean is de stelling als volgt gedefinieerd:
theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n
Het standaard build-doel FinalCheck.lean bevat:
/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms fermat_last_theorem
Dit betekent dat de build faalt tenzij het bewijs rust op exact de drie standaardaxioma's van Lean (geen sorry, geen toegevoegde axioma's, geen native_decide). FinalCheck.lean leidt daarnaast de eigen formulering van Mathlib, FermatLastTheorem, af uit deze stelling.
Hoe het is geverifieerd
Build
Er is een vanaf nul opgebouwde lake build uitgevoerd op Lean 4.33.1 (inclusief de kernel soundness-fixes van 2026), waarbij Mathlib vanuit de broncode is gecompileerd. Alle 60.475 modules van deze repository zijn gebouwd, elke declaratie is gecontroleerd door de Lean-kernel en de axioma's zijn zoals hierboven beschreven.
Comparator
leanprover/comparator v4.33.0 heeft de build gecontroleerd tegen verification/comparator/Challenge.lean, waarin de stelling uitsluitend met Mathlib wordt geformuleerd. De tool bevestigde dat de bewezen stelling en elke genoemde constante identiek zijn aan de challenge, dat er geen andere axioma's zijn gebruikt en dat het volledige bewijs, inclusief Mathlib, door de Lean-kernel wordt uitgevoerd. Verdict: Your solution is okay!
Een tweede kernel
nanoda 0.4.13, een onafhankelijke Lean-kernel geschreven in Rust, accepteerde een export van dezelfde omgeving (geschreven met lean4export). Hierbij werden 1.052.234 declaraties gecontroleerd zonder fouten. nanoda is gebouwd met vier kleine eigen patches (verification/nanoda/patches/): één voor voortgangsoutput en drie om de zoekopdracht naar definitionele gelijkheid te versnellen. Zonder deze patches zouden enkele declaraties in dit bewijs in een ongewijzigde nanoda per stuk vele uren in beslag nemen. Geen van de patches voegt, verwijdert of verzwakt een typeringregel.
Overige controles
Geen enkel module bevat axiom, sorry, nativedecide, unsafe, extern, implementedby, partial def of #eval (Challenge.lean gebruikt wel sorry bij ontwerp, maar maakt geen deel uit van het pakket).
Samen stellen deze controles vast dat de bovenstaande stelling volgt uit de drie axioma's, mits men vertrouwt op de Lean-kernel (of nanoda) en de controle-tools. De stelling is geschreven met de ingebouwde natuurlijke getallen van Lean, +, ≤, < en ≠. Het enige onderdeel van Mathlib is ^ op ℕ, wat door Mathlib is gedefinieerd als de ingebouwde exponentiatie van Lean. De comparator controleert of elke definitie die de stelling noemt identiek is aan die van de standaard Mathlib.
Wat geen tool kan controleren, is of elke tussenstelling betekent wat de naam suggereert; dit is aan de lezer om te beoordelen. PROOF-PATH.md benoemt de Lean-stelling achter elke stap en beschrijft exact hoe sterk elk genoemd klassiek resultaat is zoals hier bewezen.
Het bewijs lezen in een browser
De map html/ (ongeveer 390 MB) presenteert deze repository als statische webpagina's:
- De route van het bewijs stap voor stap.
- Een pagina voor elk van de 29.511 stellingen (de exacte Lean-stelling, wat deze citeert en wat deze citeert, en een uitvouwbare afhankelijkheidsgrafiek).
- Een pagina voor elk van de 1.450 definitiemodules (de volledige broncode en welke stellingen deze gebruiken).
- Een zoekvak voor alle stellingen- en definitiesnamen.
- De belangrijkste stellingen als een grafiek.
README.md, PROOF-PATH.md en ATTRIBUTION.md met kruisverwijzingen.
De map is onderdeel van deze repository. Open html/index.html in een webbrowser; alles werkt offline zonder webserver. De pagina's zijn uitsluitend getest in een browser op basis van Chromium. In html/README-DOCS.md wordt uitgelegd wat is geciteerd uit de Lean-bestanden en wat is gegenereerd (de Engelse samenvattingen en gesuggereerde referenties zijn automatisch gegenereerd; de Lean-stelling is leidend).
Zelf controleren
Vereisten
- Besturingssysteem: Linux of macOS (sommige paden zijn te lang voor Windows).
- Software:
elan (installeert Lean 4.33.1 via lean-toolchain).
- Netwerkverbinding: Lake haalt Mathlib op van GitHub en compileert dit uit de broncode.
Hardware en middelen
- Geheugen: De build vereist ongeveer 5 GB RAM per parallelle job (sommige modules hebben tot 36 GB nodig). Een piek van 153 GB RAM werd gemeten bij 96 jobs.
- Schijfruimte: Ongeveer 67 GB in
.lake/, plus C-bestanden (ongeveer 220 GB) die kunnen worden verwijderd tijdens het buildproces.
- Tijd: De build duurde 5 uur en 32 minuten met 96 jobs.
- Comparator: Neemt ongeveer 15 uur in beslag (gemeten: 14 uur en 46 minuten), waarvan het grootste deel de kernel-replay op één core is. Er is een piekgeheugen van 230 GB waargenomen; reken daarom op 300 GB.
- Nanoda: De export van 37,8 GB kost ongeveer 90 GB geheugen voor een uur, en de controle zelf ongeveer 40 GB (circa 30 minuten met 16 threads).
Beide scripts zijn voor Linux (bash, git, python3, GNU coreutils; nanoda vereist daarnaast patch, cargo en crates.io).
Uitvoering
git clone <this repository> flt && cd flt
LEAN_NUM_THREADS=96 lake build # standaard één job per hardware-thread; verlaag dit om geheugen te beperken (ca. 5 GB per job)
verification/comparator/run.sh # verdict: laatste regel van .verify-work/wrapper/comparator.log
verification/nanoda/run.sh # na het comparator-script; verdict: .verify-work/nanoda/run-*/nanoda.stdout
Tijdens het bouwen geeft Lean een groot aantal waarschuwingen over deprecation en stijl (linter). Deze hebben geen invloed op het resultaat. De build is geslaagd wanneer de output eindigt met: 'flt_mathlib' depends on axioms: [propext, Classical.choice, Quot.sound] and Build completed successfully.
Over de bronnen
De bestandsstructuur is als volgt opgebouwd:
FinalCheck.lean: Het standaard doel.Theorems/: Bevat de stellingen.P2M/Sol/: Bevat de bewijzen (elk importeert de stellingen die het citeert).Definitions/: Bevat de definities.verification/: Bevat de twee controles.html/: Bevat de hierboven beschreven webpagina's.tools/docs-site/: Het programma dat de webpagina's heeft gegenereerd.
De Lean-bronnen zijn geproduceerd door AI-agenten die voortbouwen op door mensen geschreven open-source Lean, met Lean als scheidsrechter. Ze zijn geschreven om gecontroleerd te worden in plaats van gelezen: namen zijn machine-gegenereerd, labels zoals P2M of hexadecimale suffixen zijn pipeline-labels en geen wiskunde. Indien een naam en een stelling verschillen, is de stelling leidend. Opmerkingen zijn verwijderd, behalve upstream-meldingen, docstrings en citaties (vermeld in ATTRIBUTION.md) en de expected-output commentaar die door #guard_msgs wordt gecontroleerd.
Licentie en attributie
Copyright 2026 Anthropic, PBC; uitgebracht onder de Apache License 2.0 (LICENSE). Delen zijn afgeleid van drie Apache-2.0 projecten die worden vermeld in NOTICE:
- Het FLT-project van het Imperial College London onder leiding van Kevin Buzzard (Frey-pakket, Galois-representaties, deformatietheorie, patching en meer).
flt-regular (Kummer's theorem).- Mathlib.
ATTRIBUTION.md bevat een lijst van 106 bestanden met materiaal uit de eerste twee projecten, inclusief bronbestand, copyrighthouder en auteurs, en 23 bestanden die Mathlib-tekst reproduceren. De webpagina's bevatten KaTeX en Graphviz (gecompileerd naar WebAssembly) onder hun eigen licenties, vermeld in html/assets/vendor/LICENSES.txt. Lean en de pakketten in lake-manifest.json worden tijdens het bouwen opgehaald en niet hier gedistribueerd.
De Laatste Stelling van Fermat in Lean 4
In het bestand PROOF-PATH.md wordt elke stap benoemd samen met de bijbehorende Lean-stelling. De map html/ presenteert het volledige bewijs als webpagina's die offline kunnen worden geraadpleegd.
Let op: Dit is een onderzoeksartifact. Het wordt niet onderhouden en er worden geen bijdragen geaccepteerd.
De stelling
In Theorems/Thmfermatlast_theorem.lean is de stelling als volgt gedefinieerd:
theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a ^ n + b ^ n ≠ c ^ n
Het standaard build-doel FinalCheck.lean bevat:
/-- info: 'fermat_last_theorem' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms fermat_last_theorem
Dit betekent dat de build faalt tenzij het bewijs rust op exact de drie standaardaxioma's van Lean (geen sorry, geen toegevoegde axioma's, geen native_decide). FinalCheck.lean leidt daarnaast de eigen formulering van Mathlib, FermatLastTheorem, af uit deze stelling.
Hoe het is geverifieerd
Build
Er is een vanaf nul opgebouwde lake build uitgevoerd op Lean 4.33.1 (inclusief de kernel soundness-fixes van 2026), waarbij Mathlib vanuit de broncode is gecompileerd. Alle 60.475 modules van deze repository zijn gebouwd, elke declaratie is gecontroleerd door de Lean-kernel en de axioma's zijn zoals hierboven beschreven.
Comparator
leanprover/comparator v4.33.0 heeft de build gecontroleerd tegen verification/comparator/Challenge.lean, waarin de stelling uitsluitend met Mathlib wordt geformuleerd. De tool bevestigde dat de bewezen stelling en elke genoemde constante identiek zijn aan de challenge, dat er geen andere axioma's zijn gebruikt en dat het volledige bewijs, inclusief Mathlib, door de Lean-kernel wordt uitgevoerd. Verdict: Your solution is okay!
Een tweede kernel
nanoda 0.4.13, een onafhankelijke Lean-kernel geschreven in Rust, accepteerde een export van dezelfde omgeving (geschreven met lean4export). Hierbij werden 1.052.234 declaraties gecontroleerd zonder fouten. nanoda is gebouwd met vier kleine eigen patches (verification/nanoda/patches/): één voor voortgangsoutput en drie om de zoekopdracht naar definitionele gelijkheid te versnellen. Zonder deze patches zouden enkele declaraties in dit bewijs in een ongewijzigde nanoda per stuk vele uren in beslag nemen. Geen van de patches voegt, verwijdert of verzwakt een typeringregel.
Overige controles
Geen enkel module bevat axiom, sorry, nativedecide, unsafe, extern, implementedby, partial def of #eval (Challenge.lean gebruikt wel sorry bij ontwerp, maar maakt geen deel uit van het pakket).
Samen stellen deze controles vast dat de bovenstaande stelling volgt uit de drie axioma's, mits men vertrouwt op de Lean-kernel (of nanoda) en de controle-tools. De stelling is geschreven met de ingebouwde natuurlijke getallen van Lean, +, ≤, < en ≠. Het enige onderdeel van Mathlib is ^ op ℕ, wat door Mathlib is gedefinieerd als de ingebouwde exponentiatie van Lean. De comparator controleert of elke definitie die de stelling noemt identiek is aan die van de standaard Mathlib.
Wat geen tool kan controleren, is of elke tussenstelling betekent wat de naam suggereert; dit is aan de lezer om te beoordelen. PROOF-PATH.md benoemt de Lean-stelling achter elke stap en beschrijft exact hoe sterk elk genoemd klassiek resultaat is zoals hier bewezen.
Het bewijs lezen in een browser
De map html/ (ongeveer 390 MB) presenteert deze repository als statische webpagina's:
- De route van het bewijs stap voor stap.
- Een pagina voor elk van de 29.511 stellingen (de exacte Lean-stelling, wat deze citeert en wat deze citeert, en een uitvouwbare afhankelijkheidsgrafiek).
- Een pagina voor elk van de 1.450 definitiemodules (de volledige broncode en welke stellingen deze gebruiken).
- Een zoekvak voor alle stellingen- en definitiesnamen.
- De belangrijkste stellingen als een grafiek.
README.md, PROOF-PATH.md en ATTRIBUTION.md met kruisverwijzingen.
De map is onderdeel van deze repository. Open html/index.html in een webbrowser; alles werkt offline zonder webserver. De pagina's zijn uitsluitend getest in een browser op basis van Chromium. In html/README-DOCS.md wordt uitgelegd wat is geciteerd uit de Lean-bestanden en wat is gegenereerd (de Engelse samenvattingen en gesuggereerde referenties zijn automatisch gegenereerd; de Lean-stelling is leidend).
Zelf controleren
Vereisten
- Besturingssysteem: Linux of macOS (sommige paden zijn te lang voor Windows).
- Software:
elan (installeert Lean 4.33.1 via lean-toolchain).
- Netwerkverbinding: Lake haalt Mathlib op van GitHub en compileert dit uit de broncode.
Hardware en middelen
- Geheugen: De build vereist ongeveer 5 GB RAM per parallelle job (sommige modules hebben tot 36 GB nodig). Een piek van 153 GB RAM werd gemeten bij 96 jobs.
- Schijfruimte: Ongeveer 67 GB in
.lake/, plus C-bestanden (ongeveer 220 GB) die kunnen worden verwijderd tijdens het buildproces.
- Tijd: De build duurde 5 uur en 32 minuten met 96 jobs.
- Comparator: Neemt ongeveer 15 uur in beslag (gemeten: 14 uur en 46 minuten), waarvan het grootste deel de kernel-replay op één core is. Er is een piekgeheugen van 230 GB waargenomen; reken daarom op 300 GB.
- Nanoda: De export van 37,8 GB kost ongeveer 90 GB geheugen voor een uur, en de controle zelf ongeveer 40 GB (circa 30 minuten met 16 threads).
Beide scripts zijn voor Linux (bash, git, python3, GNU coreutils; nanoda vereist daarnaast patch, cargo en crates.io).
Uitvoering
git clone <this repository> flt && cd flt
LEAN_NUM_THREADS=96 lake build # standaard één job per hardware-thread; verlaag dit om geheugen te beperken (ca. 5 GB per job)
verification/comparator/run.sh # verdict: laatste regel van .verify-work/wrapper/comparator.log
verification/nanoda/run.sh # na het comparator-script; verdict: .verify-work/nanoda/run-*/nanoda.stdout
Tijdens het bouwen geeft Lean een groot aantal waarschuwingen over deprecation en stijl (linter). Deze hebben geen invloed op het resultaat. De build is geslaagd wanneer de output eindigt met: 'flt_mathlib' depends on axioms: [propext, Classical.choice, Quot.sound] and Build completed successfully.
Over de bronnen
De bestandsstructuur is als volgt opgebouwd:
FinalCheck.lean: Het standaard doel.Theorems/: Bevat de stellingen.P2M/Sol/: Bevat de bewijzen (elk importeert de stellingen die het citeert).Definitions/: Bevat de definities.verification/: Bevat de twee controles.html/: Bevat de hierboven beschreven webpagina's.tools/docs-site/: Het programma dat de webpagina's heeft gegenereerd.
De Lean-bronnen zijn geproduceerd door AI-agenten die voortbouwen op door mensen geschreven open-source Lean, met Lean als scheidsrechter. Ze zijn geschreven om gecontroleerd te worden in plaats van gelezen: namen zijn machine-gegenereerd, labels zoals P2M of hexadecimale suffixen zijn pipeline-labels en geen wiskunde. Indien een naam en een stelling verschillen, is de stelling leidend. Opmerkingen zijn verwijderd, behalve upstream-meldingen, docstrings en citaties (vermeld in ATTRIBUTION.md) en de expected-output commentaar die door #guard_msgs wordt gecontroleerd.
Licentie en attributie
Copyright 2026 Anthropic, PBC; uitgebracht onder de Apache License 2.0 (LICENSE). Delen zijn afgeleid van drie Apache-2.0 projecten die worden vermeld in NOTICE:
- Het FLT-project van het Imperial College London onder leiding van Kevin Buzzard (Frey-pakket, Galois-representaties, deformatietheorie, patching en meer).
flt-regular (Kummer's theorem).- Mathlib.
ATTRIBUTION.md bevat een lijst van 106 bestanden met materiaal uit de eerste twee projecten, inclusief bronbestand, copyrighthouder en auteurs, en 23 bestanden die Mathlib-tekst reproduceren. De webpagina's bevatten KaTeX en Graphviz (gecompileerd naar WebAssembly) onder hun eigen licenties, vermeld in html/assets/vendor/LICENSES.txt. Lean en de pakketten in lake-manifest.json worden tijdens het bouwen opgehaald en niet hier gedistribueerd.
Groetjes,