A formal proof of the Ramanujan--Nagell theorem in Lean 4

Dit artikel presenteert een volledige formalisatie in Lean 4 van de stelling van Ramanujan-Nagell, die de enige geheeltallige oplossingen voor de Diophantische vergelijking $x^2 + 7 = 2^n$ identificeert, inclusief de benodigde algebraïsche getaltheoretische infrastructuur en een analyse van de uitdagingen bij het vertalen van bewijzen naar machine-verifieerbare code.

De kern

Stel je voor dat wiskunde een enorme, onontgonnen jungle is. In deze jungle liggen oude, mysterieuze schatten: formules en vergelijkingen die wiskundigen al eeuwen proberen op te lossen. Een van die schatten is de Ramanujan-Nagell-stelling.

Deze stelling gaat over een heel specifieke puzzel: Welke getallen kun je invullen in de formule $x^2 + 7 = 2^n$ zodat het resultaat een heel getal is?

De Indiase wiskundige Ramanujan dacht in 1913 dat hij de oplossing had gevonden, maar hij kon het niet bewijzen. Later, in 1948, bewees de Noorse wiskundige Nagell dat hij gelijk had: er zijn maar vijf mogelijke antwoorden. Het probleem? Het bewijs was geschreven in de taal van mensen: met woorden, intuïtie en "het is duidelijk dat..."-zinnen. Voor een computer is "het is duidelijk" vaak het ergste woordje dat je kunt gebruiken.

Dit artikel vertelt het verhaal van Barinder Banwait, die deze menselijke bewijzen heeft vertaald naar een taal die een computer perfect begrijpt: Lean 4. Hij heeft de jungle niet alleen verkend, maar elke stap van het pad exact uitgemeten en vastgezet in een digitaal net.

Hier is hoe hij dat gedaan heeft, vertaald in alledaagse termen:

1. De Bouwvakkers en de Blauwdruk

Om een huis te bouwen, heb je niet alleen een ontwerper nodig, maar ook een stevige fundering. In de wiskunde is die fundering de algebraïsche getaltheorie.

• De Menselijke Versie: Een wiskundige kijkt naar een vergelijking en zegt: "We werken hier in een speciaal getallenstelsel (een 'ring van gehele getallen'). Die is heel netjes, alles valt daar perfect in elkaar."
• De Computer-Versie: De computer vraagt: "Welke regels gelden daar precies? Wat is de naam van die ring? Wat zijn de eenheden? Is het echt netjes?"
  Banwait moest eerst een heel nieuw gereedschapskistje bouwen voor de computer. Hij bouwde een digitale versie van het getallenstel $\mathbb{Q}(\sqrt{-7})$. Het is alsof hij eerst een compleet nieuw soort bakstenen en cement moest uitvinden voordat hij de muur kon optrekken.

2. Het Dubbele Spoor (De Isomorfisme)

Een van de grootste valkuilen was een soort "twee sporen" probleem.

• De Analogie: Stel je voor dat je een stad noemt "Amsterdam". Maar in het ene boek wordt de stad beschreven vanuit het Centraal Station, en in het andere boek vanuit de Dam. Voor een mens is het duidelijk dat het dezelfde stad is. Voor een computer zijn het twee totaal verschillende adressen.
• Het Probleem: De wiskundigen gebruikten één manier om het getallenstel te beschrijven, maar de computer (Lean) had een andere manier nodig om het te berekenen. Banwait moest een digitale brug bouwen tussen deze twee versies, zodat de computer begreep: "Ah, dit is echt hetzelfde getallenstel, alleen anders verpakt."

3. De "Drie Getallen" en de 42-Regel

Het hart van het bewijs is een slimme truc.

• De Menselijke Logica: Als je de vergelijking uitrekent, zie je dat het antwoord alleen kan kloppen als het getal $n$ een heel specifiek soort getal is. Het moet overblijven bij delen door 42 op een van drie manieren (net als een getal dat op een uurwerk altijd op 3, 5 of 13 uur moet staan).
• De Uitdaging: In een menselijk bewijs zeg je: "Als je dit uitrekent, zie je dat..." en dan spring je naar de conclusie. Voor de computer moet je elke stap van die uitrekening stap voor stap uitleggen. Banwait moest de computer dwingen om duizenden kleine berekeningen te doen om te bewijzen dat er echt geen andere opties zijn. Het is alsof je een detective bent die niet mag zeggen "de dader was hier", maar elke voetstap, elk zweetdruppel en elke stofdeeltje moet analyseren om het te bewijzen.

4. De AI-assistenten: De Digitale Hulpjes

Dit is misschien wel het meest spannende deel van het verhaal. Banwait werkte niet alleen. Hij gebruikte kunstmatige intelligentie (AI) als zijn persoonlijke assistent.

• De Rol van de AI: Stel je voor dat je een heel moeilijk raadsel oplost. Je hebt een slimme robot die naast je zit. Als je vastloopt, zegt de robot: "Probeer eens deze knop in te drukken" of "Ik heb net gezien dat er een boek is met de oplossing voor dit specifieke stukje."
• Wat deed de AI?
  • Het suggereerde de juiste stappen voor de computer.
  • Het hielp bij het zoeken in de enorme bibliotheek van wiskundige regels (Mathlib).
  • Het schreef de saaie, repetitieve stukken code voor, zodat Banwait zich kon focussen op de moeilijke logica.
  • Belangrijk: De AI was de schrijver, maar de computer (Lean) was de controleur. De AI kon liegen of fouten maken, maar de computer checkte elke zin tot op de bodem. Als de computer het niet accepteerde, was het bewijs niet geldig.

Waarom is dit belangrijk?

Vroeger waren wiskundige bewijzen zoals een recept in een kookboek: "Voeg een snufje zout toe." Als je het recept van een meesterkok volgt, lukt het meestal wel, maar je weet niet precies hoeveel zout er in zat.

Met dit project heeft Banwait het recept omgezet in een exacte chemische formule: "Voeg precies 0,045 gram zout toe."

• Betrouwbaarheid: We weten nu 100% zeker dat de Ramanujan-Nagell-stelling klopt. Er is geen ruimte meer voor menselijke fouten of misverstanden.
• De Toekomst: Dit is de eerste keer dat een beroemde Ramanujan-voorstelling volledig door een computer is geverifieerd. Het is een mijlpaal. Het laat zien dat we met de hulp van AI en slimme software complexe wiskundige mysteries kunnen oplossen die te groot zijn voor één menselijk brein om zonder fouten te controleren.

Kortom: Banwait heeft een brug gebouwd tussen de intuïtieve wereld van de menselijke wiskunde en de strikt logische wereld van de computer, met een beetje hulp van slimme robots. En aan het andere eind van die brug staat een bewijs dat nooit meer in twijfel getrokken kan worden.

Technische samenvatting

Titel: Een formeel bewijs van de Ramanujan–Nagell-stelling in Lean 4

Auteur: Barinder S. Banwait
Context: Publicatie in Lean 4 met de Mathlib-bibliotheek.

---

1. Het Probleem

De Ramanujan–Nagell-stelling betreft een specifieke Diophantische vergelijking:
$$x^2 + 7 = 2^n$$
waarbij $x$ en $n$ gehele getallen zijn.
Ramanujan stelde in 1913 de vraag voor welke waarden van $n$ de uitdrukking $2^n - 7$ een perfect kwadraat is. Hij gaf de oplossingen $n \in \{3, 4, 5, 7, 15\}$ en suggereerde dat dit de enige oplossingen zijn. Dit werd in 1948 bewezen door Trygve Nagell.

Het doel van dit artikel is het volledig formeel verifiëren van dit bewijs in een interactieve bewijshulpmiddel (Lean 4), inclusief alle onderliggende wiskundige infrastructuren die in handboeken vaak als "zelfsprekend" worden beschouwd.

2. Methodologie en Architectuur

Het bewijs is geïmplementeerd in Lean 4 met gebruikmaking van de Mathlib-bibliotheek. De formalisatie is opgebouwd uit vijf bestanden en volgt de klassieke bewijsstrategie uit de algebraïsche getaltheorie, maar met een strikte nadruk op machine-gecontroleerde logica.

De Bewijsstrategie (Korte weergave)

1. Even $n$: Directe factorisatie toont aan dat $n=4$ en $x=\pm 3$ de enige oplossing is.
2. Oneven $n$:
   • De vergelijking wordt herschreven in het kwadratische getalveld $K = \mathbb{Q}(\sqrt{-7})$.
   • De ring van gehele getallen $\mathcal{O}_K$ wordt geïdentificeerd als $\mathbb{Z}[\frac{1+\sqrt{-7}}{2}]$.
   • Omdat $\mathcal{O}_K$ een Unieke Factorisatie Domein (UFD) is, kan de vergelijking worden ontbonden in irreducibele elementen $\theta$ en $\theta'$.
   • Dit leidt tot de vergelijking $\pm\sqrt{-7} = \theta^m - \theta'^m$ (waarbij $m = n-2$).
   • Door gebruik te maken van binomiale expansie en modulair rekenen (modulo 7 en 42), wordt bewezen dat $m$ slechts drie mogelijke restklassen modulo 42 kan hebben.
   • Een uniciteitsargument (gebaseerd op 7-adische waarderingen) toont aan dat elke restklasse hooguit één oplossing oplevert.

Architectuur van de Formalisatie

De code is verdeeld in twee lagen:

1. Infrastructuur (Algebraïsche Getaltheorie):
   • QuadraticIntegerROI.lean: Generaliseert de identificatie van de ring van gehele getallen voor $d \equiv 1 \pmod 4$.
   • RingOfIntegers.lean & FieldIsomorphism.lean: Specificeert dit voor $d=-7$ en bouwt een isomorfisme tussen twee verschillende representaties van het veld $\mathbb{Q}(\sqrt{-7})$ (één met generator $\sqrt{-7}$, één met $\frac{1+\sqrt{-7}}{2}$).
   • Helpers.lean: Berekent de discriminant, bewijst dat de klasgetal 1 is (dus een Hoofdideaaldomein), bepaalt de eenheidsgroep ($\{\pm 1\}$), en bewijst irreducibiliteit.
2. Het Eigenlijke Bewijs:
   • Basic.lean: Implementeert de factorisatie, de modulair-reductie (mod 42) en het uniciteitsbewijs.

Statistieken:

• Totaal: 3.570 regels code (LOC).
• Aantal declaraties: 125 (definities, lemmata, theorema's).
• Geen gebruik van sorry (geen onbewezen aannames); het bewijs is volledig compleet.

3. Belangrijkste Bijdragen

1. Eerste Formele Bewijs van een Ramanujan-conjectuur: Dit is het eerste keer dat een conjectuur van Ramanujan volledig is geverifieerd in een bewijshulpmiddel.
2. Volledige Oplossing van een Exponentiële Diophantische Vergelijking: De eerste complete oplossing van dit specifieke type vergelijking in een formeel verificatiesysteem.
3. Infrastructuur voor $\mathbb{Q}(\sqrt{-7})$: De auteur heeft een robuuste basis gelegd voor werken met de ring van gehele getallen van dit specifieke kwadratische veld, inclusief:
   • Identificatie als een kwadratische integer-ring.
   • Verificatie van unieke factorisatie (via het bewijs dat de klasgetal 1 is).
   • Bepaling van de eenheidsgroep.
   • Deze infrastructuur is ontworpen om generaliseerbaar te zijn naar andere kwadratische velden.
4. Analyse van de "Gap": Het artikel analyseert kritisch waar de kloof tussen handmatige wiskundige bewijzen en machine-gecontroleerde bewijzen ligt, en identificeert specifieke obstakels in de formalisatie.

4. Technische Uitdagingen en Resultaten

De auteur identificeert vier hoofdgebieden waar de formalisatie aanzienlijk meer werk vereiste dan het handmatige bewijs:

• Isomorfismen en Integraliteit: In wiskundige teksten worden verschillende representaties van hetzelfde veld ($\sqrt{-7}$ vs. $\frac{1+\sqrt{-7}}{2}$) als gelijk beschouwd. In Lean zijn dit echter verschillende types. Het bouwen van een expliciete isomorfisme en het "transporteren" van eigenschappen (zoals de integraliteit van de ring) vereiste aanzienlijke inspanning.
• Typeclass-inferentie: Het systeem van typeclasses in Lean veroorzaakte "diamonds" (conflicten tussen verschillende manieren om een algebraïsche structuur te definiëren). Dit vereiste handmatige ingrepen om te garanderen dat het systeem de juiste instanties kende.
• Bepaling van de Eenheidsgroep: Het bewijzen dat de enige eenheden $\pm 1$ zijn, was verrassend arbeidsintensief. Hoewel Dirichlet's eenheidstelling beschikbaar was in Mathlib, vereiste het elimineren van specifieke cyclotomische gevallen (orde 3, 4, 6) uitgebreid rekenwerk met Diophantische vergelijkingen in de ring, wat leidde tot lange bewijzen (ca. 236 regels).
• Rekenen in $\mathcal{O}_K$ vs. $\mathbb{Z}$: Bewijzen die in de gehele getallen ($\mathbb{Z}$) triviaal zijn, vereisten in de ring van gehele getallen van het kwadratische veld complexe coercies (omzettingen) en herschrijvingen. De tactic linarith werkt niet direct op deze ringen, waardoor handmatige normalisatie nodig was.

Resultaat:
Het bewijs bevestigt dat de enige oplossingen voor $x^2 + 7 = 2^n$ zijn:
$$(n, x) \in \{(3, \pm 1), (4, \pm 3), (5, \pm 5), (7, \pm 11), (15, \pm 181)\}$$

5. Betekenis en Toekomstperspectief

• Rol van AI: Een opvallend aspect van dit project is het uitgebreide gebruik van generatieve AI-tools (Claude Code en Aristotle). Deze tools hielpen bij:
  • Het suggereren van tactieken.
  • Het repareren van bewijzen bij updates van de Mathlib-bibliotheek.
  • Het vinden van relevante lemmata in de grote API.
  • Het genereren van repetitieve "boilerplate" code.
    De auteur concludeert dat AI de drempel voor formalisatie aanzienlijk verlaagt, hoewel de kern van Lean (de kernel) de uiteindelijke correctheid garandeert.
• Impact op Algebraïsche Getaltheorie: Dit werk toont aan dat complexe theorieën uit de algebraïsche getaltheorie (zoals klasgetallen, eenheidsgroepen en 7-adische waarderingen) nu volledig formaliseerbaar zijn. Het legt de basis voor het formaliseren van nog complexere stellingen in dit domein.
• Beschikbaarheid: De volledige code, inclusief een interactief afhankelijkheidsdiagram en een "proof blueprint", is publiek beschikbaar gemaakt.

Conclusie:
Dit artikel markeert een mijlpaal in het veld van formeel bewijs. Het combineert diepgaande wiskundige theorie met state-of-the-art software-engineering en AI-assistentie om een klassiek probleem uit de getaltheorie volledig op te lossen en te verifiëren, terwijl het tegelijkertijd waardevolle inzichten biedt in de praktische uitdagingen van het vertalen van wiskunde naar code.