💻 computer science

A formalization of the Gelfond-Schneider theorem

Dit artikel beschrijft de formalisatie van Hilberts zevende probleem en de Gelfond-Schneider-stelling in de Lean 4-bewijshulpmiddel, die stelt dat $\alpha^\beta$ transcendent is voor algebraïsche getallen $\alpha \neq 0,1$ en irrationale algebraïsche $\beta$ .

Oorspronkelijke auteurs: Michail Karatarakis, Freek Wiedijk

Gepubliceerd 2026-03-27

📖 4 min leestijd☕ Koffiepauze-leesvoer

CC BY 4.0

Oorspronkelijke auteurs: Michail Karatarakis, Freek Wiedijk

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat wiskunde een enorme bibliotheek is vol met getallen. In deze bibliotheek zijn er twee grote afdelingen: de algebraïsche getallen en de transcendente getallen.

Algebraïsche getallen zijn als de "normale" bewoners. Ze zijn getallen die je kunt vinden door met gewone gehele getallen (1, 2, 3...) te rekenen en vergelijkingen op te lossen. Denk aan breuken zoals 1/2 of wortels zoals $\sqrt{2}$ . Ze hebben een duidelijke "adres" in de wiskunde.
Transcendente getallen zijn de "vreemde" bewoners. Ze passen in geen enkele vergelijking met gewone getallen. Ze zijn onvoorspelbaar en oneindig complex. De beroemdste voorbeelden zijn $\pi$ (pi) en $e$ .

Het Grote Raadsel
In 1900 stelde de beroemde wiskundige David Hilbert een lijst op met de 23 moeilijkste raadsels ter wereld. Het zevende raadsel ging over een specifieke combinatie: wat gebeurt er als je een algebraïsch getal (zoals 2) tot de macht van een ander getal (zoals $\sqrt{2}$ ) verheft?
Is het resultaat dan nog steeds een "normaal" getal, of wordt het een "vreemd" transcendent getal?
Hilbert dacht dat dit raadsel misschien wel 100 jaar zou duren om op te lossen. Maar in 1934 losten twee wiskundigen, Gelfond en Schneider, het op. Hun stelling (het Gelfond-Schneider-theorema) zegt simpelweg:

Als je een getal neemt dat niet 0 of 1 is, en je verheft het tot een macht die een "vreemd" irrationaal getal is, dan is het resultaat altijd een transcendent getal.

De Uitdaging: Bewijzen met een Computer
Nu is het bewijzen van zo'n ding met pen en papier al heel moeilijk. Maar wat als je het wilt laten bewijzen door een computer? Dat is wat deze twee auteurs, Michail en Freek, hebben gedaan. Ze hebben het bewijs in het programma Lean geschreven.

Lean is als een superstrengere leraar. Als jij in een normaal wiskundig boek zegt "en dan is het duidelijk dat...", zegt Lean: "Nee, leg dat stap voor stap uit, want ik zie het niet."

Hoe hebben ze het gedaan? (De Analogie)
Het bewijs is als het bouwen van een onbreekbaar kasteel om een dief (het getal dat we willen bewijzen) te vangen.

De Valstrik (De Hulpfunctie):
De wiskundigen bouwen een speciaal wiskundig apparaat, een "hulpfunctie". Stel je dit voor als een gigantisch web dat ze in de lucht spannen. Ze berekenen de draden van dit web zo precies, dat het web op bepaalde plekken (de getallen 1, 2, 3...) plat op de grond moet liggen (waarde 0).
Om dit web te bouwen, gebruiken ze een truc genaamd Siegel's Lemma. Dit is als een magische sleutel die zegt: "Als je genoeg onbekende schroeven hebt en minder gaten dan schroeven, dan kun je altijd een manier vinden om de schroeven zo te draaien dat het web perfect past."
De Twee Kanten van de Munt:
Nu hebben ze dit web. Ze kijken naar één specifiek punt in het web.
- De Wiskundige kant: Omdat het web uit "normale" getallen is gebouwd, mag het op dat punt niet te klein zijn. Het moet een zekere kracht hebben.
- De Analyse kant: Maar door de manier waarop ze het web hebben ontworpen, zou het op dat punt extreem klein moeten zijn, bijna nul.
De Klap:
Hier komt de magie. Als je de twee berekeningen naast elkaar zet, krijg je een onmogelijke situatie. Het getal moet tegelijkertijd groot genoeg zijn om te bestaan, en klein genoeg om bijna te verdwijnen.
Dit is een tegenstrijdigheid. Het enige wat er dan overblijft, is dat onze oorspronkelijke aanname fout was. We dachten dat het resultaat een "normaal" getal was. Maar omdat dat leidt tot een onmogelijkheid, moet het resultaat wel een "vreemd" transcendent getal zijn.

Waarom is dit belangrijk?
Vroeger waren bewijzen als dit alleen te controleren door andere wiskundigen die jarenlang naar de pagina's staarden. Als er één klein foutje in zat, kon het jaren duren om het te vinden.
Door dit in Lean te zetten, hebben de auteurs het bewijs 100% foutloos gemaakt. De computer heeft elke stap gecontroleerd.

Ze hebben niet alleen het theorema bewezen, maar ook de "hulpstukken" (zoals de meetkunde van complexe getallen) in de computerbibliotheek gezet.
Ze hebben laten zien dat zelfs de beroemde "Gelfond-Schneider-constante" ( $\sqrt{2}^{\sqrt{2}}$ ) inderdaad transcendent is.

Conclusie
Dit paper is als het leggen van de eerste steen voor een nieuwe brug. Ze hebben de basis gelegd om in de toekomst nog complexere wiskundige mysteries op te lossen met computers. Het laat zien dat zelfs de oudste en moeilijkste raadsels van de wiskunde, als je ze maar klein genoeg maakt en stap voor stap uitlegt, door een machine kunnen worden begrepen en bewezen. Het is een overwinning voor de menselijke geest, versterkt door de onfeilbaarheid van de computer.

Titel: Een formalisering van de stelling van Gelfond-Schneider

Auteurs: Michail Karatarakis en Freek Wiedijk (Radboud Universiteit)
Context: Geformaliseerd in Lean 4 (Mathlib), gepresenteerd tijdens het "Prospects of Formal Mathematics" programma aan het Hausdorff Institute for Mathematics (HIM).

1. Het Probleem: Hilbert's Zevende Probleem

Het artikel richt zich op de formalisering van Hilbert's Zevende Probleem, gesteld in 1900. Het probleem vraagt om de aard (algebraïsch of transcendent) te bepalen van getallen van de vorm $\alpha^\beta$ , waarbij:

$\alpha$ en $\beta$ algebraïsche getallen zijn.
$\alpha \notin \{0, 1\}$ .
$\beta$ irrationaal is.

De stelling van Gelfond-Schneider (onafhankelijk bewezen in 1934 door Gelfond en Schneider) stelt dat onder deze voorwaarden $\alpha^\beta$ altijd een transcendent getal is. Dit is een fundamenteel resultaat in de getaltheorie dat algebraïsche getaltheorie en complexe analyse verbindt. Voorbeelden van transcendent getallen die hieruit volgen zijn $2^{\sqrt{2}}$ , $e^\pi$ (Gelfonds constante) en $i^i$ .

Hoewel er eerdere mechaniseringen waren voor de transcendentie van specifieke constanten (zoals $e$ en $\pi$ ) en voor Liouville-getallen, was er tot nu toe geen volledige mechanisatie van de stelling van Gelfond-Schneider in een bewijshulpmiddel (proof assistant).

2. Methodologie en Implementatie

De auteurs hebben het bewijs volledig geïmplementeerd in Lean 4, gebruikmakend van de Mathlib-bibliotheek. Het project volgt de klassieke bewijsstrategie, maar vereist een strikte, constructieve aanpak binnen de beperkingen van type-theorie.

A. Algebraïsche Basis (Sectie 2)

Het bewijs vereist geavanceerde algebraïsche getaltheorie:

Het "House" van een algebraïsch getal: In plaats van een simpele definitie op basis van de wortels van een polynoom (wat ordeningsproblemen veroorzaakt), definiëren de auteurs het "house" (de maximale modulus van de geconjugeerden) via een canonieke inbedding in een Banach-algebra. Dit maakt gebruik van de bestaande normed space API in Mathlib, wat het bewijzen van ongelijkheden (zoals de driehoeksongelijkheid) aanzienlijk vereenvoudigt.
Siegel's Lemma voor getallenlichamen: Het klassieke lemma (voor rationale gehele getallen) is al in Mathlib aanwezig. De auteurs hebben dit echter gegeneraliseerd naar het ring van algebraïsche gehele getallen ( $\mathcal{O}_K$ ) van een getallenlichaam $K$ . Ze gebruiken een "descent"-argument om het lineaire systeem over $\mathcal{O}_K$ om te zetten naar een groter systeem over $\mathbb{Z}$ , oplossen met het klassieke lemma, en het resultaat weer "liften" naar $\mathcal{O}_K$ . Dit garandeert het bestaan van kleine, niet-triviale algebraïsche gehele coëfficiënten voor een hulpfunctie.

B. Analytische Kern en de Hulpfunctie (Sectie 3)

Het hart van het bewijs is de constructie van een hulpfunctie $R(z)$ die op specifieke punten een hoge orde van verdwijning heeft.

Constructie van $R(z)$ : De coëfficiënten van $R(z)$ worden bepaald door een onderbepaald stelsel lineaire vergelijkingen. Siegel's Lemma garandeert dat er een oplossing bestaat met coëfficiënten die "klein" zijn (gemeten in hun "house").
De globale functie $S(z)$ : Een cruciale en technisch uitdagende stap is de formalisering van de functie $S(z)$ $S (z)$ , die nodig is voor de Cauchy-integraalformule.
- Klassiek: $S(z)$ wordt gedefinieerd als een quotiënt met polen op gehele getallen, waarbij men aannam dat deze polen "verwijderbaar" zijn en men ze simpelweg vermijdt.
- In Lean: Een meromorfe definitie is problematisch omdat het domein van definitie en het vermijden van polen expliciet bewezen moeten worden. De auteurs hebben $S(z)$ $S (z)$ daarom geconstrueerd als een totale, stuksgewijs holomorfe functie. Ze gebruiken een "patching"-strategie:
  1. Bepalen van lokale holomorfe factoren rond de singulariteiten.
  2. Definieren van de functie op de singulariteiten via deze lokale factoren.
  3. Aantonen dat deze stukken analytisch "naadloos" aansluiten op de rationale definitie daarbuiten.
    Dit bewijst dat $S(z)$ overal analytisch is, wat essentieel is voor de toepassing van Cauchy's integraalformule.

C. Het Contradictie-argument

Het bewijs loopt via een contradictie:

Aanneming: Stel $\alpha^\beta$ is algebraïsch.
Aritmetische ondergrens: Omdat de afgeleide van de hulpfunctie op een specifiek punt een algebraïsch getal is (en niet nul), moet de norm van dit getal (over het rationale veld) minstens 1 zijn. Dit levert een ondergrens op die exponentieel groeit met de parameters.
Analytische bovengrens: Door Cauchy's integraalformule toe te passen op de geconstrueerde functie $S(z)$ , kan een bovengrens worden afgeleid die super-exponentieel afneemt (of langzamer groeit dan de ondergrens) als de parameters groot worden.
Conclusie: Voor voldoende grote parameters is de analytische bovengrens strikt kleiner dan de arithmetische ondergrens, wat een contradictie oplevert. De aanname dat $\alpha^\beta$ algebraïsch is, is dus onjuist.

3. Belangrijkste Bijdragen

Eerste formalisering: Dit is, voor zover bekend, de eerste volledige mechanisatie van de stelling van Gelfond-Schneider in een bewijshulpmiddel.
Geavanceerde complexe analyse in Lean: De implementatie van de totale functie $S(z)$ met verwijderbare singulariteiten is een mijlpaal in de formalisering van complexe analyse binnen type-theorie. Het lost het probleem op van het werken met meromorfe functies zonder expliciete domeinbeperkingen.
Expliciete constanten: In tegenstelling tot klassieke bewijzen die vaak $O(\cdot)$ -notatie of generieke constanten gebruiken, hebben de auteurs een reeks van 15 expliciete constanten ( $c_1$ tot $c_{15}$ ) afgeleid en bijgehouden. Dit is noodzakelijk om de strikte ongelijkheden in Lean te bewijzen en vormt een basis voor kwantitatieve resultaten.
Integratie in Mathlib: Onderdelen van de code, zoals de definitie van het "house" en de generalisatie van Siegel's Lemma, zijn al geïntegreerd in de Mathlib-bibliotheek, wat de infrastructuur voor toekomstige getaltheoretische bewijzen verrijkt.

4. Resultaten

De stelling is formeel bewezen: Voor algebraïsche $\alpha \notin \{0,1\}$ en irrationale algebraïsche $\beta$ is $\alpha^\beta$ transcendent.
Als sanity-check is de transcendentie van de Gelfond-Schneider constante ( $\sqrt{2}^{\sqrt{2}}$ ) formeel afgeleid.
De code is openbaar beschikbaar op een Mathlib-branch.

5. Betekenis en Toekomstperspectief

Deze werken legt de basis voor verdere formalisaties in de transcendentie-theorie:

Baker's Stelling: De volgende logische stap is het formaliseren van Baker's stelling over lineaire vormen in logaritmen, die de stelling van Gelfond-Schneider generaliseert.
p-adische versies: De algebraïsche structuur van het bewijs is onafhankelijk van de complexe inbedding. Door complexe analyse te vervangen door p-adische analyse (Schnirelmann-integrals), zou de p-adische versie van de stelling kunnen worden bewezen.
Schneider-Lang stelling: De technieken (hulpfuncties, Siegel's Lemma) zijn centraal in het bewijs van de Schneider-Lang stelling, die transcendentie resultaten uitbreidt naar meromorfe functies die voldoen aan algebraïsche differentiaalvergelijkingen.
Beslissingsprocedures: De expliciete constanten maken het mogelijk om in de toekomst beslissingsprocedures te ontwikkelen voor specifieke klassen van transcendent getallen, mogelijk geautomatiseerd via intervalrekenen.

Kortom, dit artikel markeert een overgang van het formaliseren van geïsoleerde stellingen naar het opbouwen van een robuust theoretisch kader voor diepe resultaten in de getaltheorie binnen Lean.