An English version is also available.
Het eerste gezichtsbepalende probleem voor het informaticaonderzoek uit een lijst van tien dergelijke problemen opgesteld door prof dr Jan Bergstra, zie [NOAG-ict] blz. 52 luidt:
"Formaliseer en controleer per computer een bewijs van het door Wiles aangetoonde vermoeden van Fermat. Deze vraagstelling bouwt voort op een lange en sterke Nederlands traditie."
Ik zal op deze webpagina proberen een aantal van de aspecten van dit probleem uiteen te zetten en enige literatuur en links naar relevante websites te geven.
Pierre de Fermat schreef rond 1640 in de kantlijn van zijn Latijnse vertaling van Diophantos' werk een opmerking die we tegenwoordig als volgt weergeven:
Stelling. De vergelijking an + bn = cn heeft voor gehele getallen a, b, c, ongelijk 0, en n > 2 geen oplossingen.
Terzijde, de betreffende passage van Diophantos ging over het geval n=2. Er zijn dan oneindig veel oplossingen, bv. 42 + 32 = 52 en 122 + 52 = 132.
De notities van Fermat zijn na zijn dood uitgegeven door zijn zoon. Fermats opmerking, dat hij er een fraai bewijs voor had, berust volgens [Struik] waarschijnlijk op een vergissing. Fermat bewees volgens Stevens [CSS] wel het geval n = 4. Het geval n = 3 werd door Leonhard Euler (ca. 1760) bewezen. Het geval n=5 werd in 1825 opgelost door Legendre en Dirichlet. In 1847 beweees Kummer alle gevallen waarin n een zogenaamd regulier priemgetal is (het kleinste niet-reguliere priemgetal is 37). Zie [Edwards] voor de bewijzen voor n = 3 en 4 , en voor de reguliere priemgetallen. In 1976 gold het vermoeden van Fermat reeds voor alle gevallen met n kleiner dan miljoen [Wagstaff].
Andrew Wiles kondigde in 1993 aan dat hij de Stelling van Fermat bewezen had. Er bleek toen nog een gat in het bewijs te zitten, maar dat heeft hij samen met Taylor in 1995 gedicht. Dit werk is gepubliceerd in [Wiles, TaWi]. De beste bron is thans het boek [CSS]. Veel leesbaarder is [vdP], dit boek leest voor een wiskundige welhaast als Dan Browns Da Vinci Code.
Fermats vermoeden is eigenlijk niet meer dan een curiositeit. Het heeft in de geschiedenis van de wiskunde een belangrijke rol gespeeld als inspiratiebron of toetssteen voor wiskundige theorieen. Fermats vermoeden is onderdeel van de getaltheorie, een tak van wiskunde die tot in de jaren 70 van de vorige eeuw beschouwd werd als maatschappelijk nutteloos, maar goed voor wiskundigen om het vak te leren.
Tegenwoordig is getaltheorie maatschappelijk van groot belang, omdat het wordt toegepast in de cryptografie, de wetenschap van het veilig overzenden en bewaren van vertrouwelijke en waardevolle gegevens over bv. het internet. Voorzover ik weet heeft het vermoeden van Fermat echter geen directe cryptografische toepassingen.
Het bewijs van Wiles is belangrijker dan Fermats vermoeden.
Wiles bewijst Fermats vermoeden namelijk door een deel van het
Modulariteitsvermoeden van Shimura, Taniyama en Weil te
bewijzen. Dit vermoeden ontstond tussen 1957 en 1967. Het houdt in,
dat elke elliptische kromme met rationale coëfficienten
tevens een modulaire kromme is. Een dergelijk resultaat is
belangrijk omdat het verschillende deelgebieden van de wiskunde met
elkaar in verband brengt. Overigens heeft ook dit resultaat bij mijn
weten geen directe gevolgen in de cryptografie.
Terug naar de aspecten.
Ik volg de schets van Stevens (of Serre) in [CSS]. Het bewijs bestaat uit een elementair deel, de stellingen 1 tot en met 4 hieronder, en een deel dat veel diepere wiskunde vereist: de stellingen 5, 6 en 7. Ik geef hier de bewijzen van stellingen 1 en 4. Zie bv [Edwards] voor de bewijzen van de stellingen 2 en 3. In de stellingen 5, 6 en 7 komen allerlei cursief afgedrukte begrippen voor, die ik niet kan uitleggen. Eerst twee definities die vermoedelijk wel bekend zijn, gevolgd door een afspraak waardoor we de zinnen wat korter kunnen houden.
Een priemgetal is een geheel getal > 1, dat geen andere
delers heeft dan 1 en zichzelf.
Twee gehele getallen heten relatief
priem als hun grootste gemene deler 1 is (oftewel als ze geen
gemeenschappelijke deler > 1 hebben).
We noemen een drietal gehele getallen (a,b,c) ongelijk 0 een Fermat-drietal bij exponent n indien an + bn = cn en n > 2. We willen bewijzen dat Fermat-drietallen niet bestaan. Dit gebeurt door uit te gaan van het bestaan van een Fermat-drietal bij exponent n, en dan een tegenspraak af te leiden.
Stelling 1. Als er een Fermat-drietal bij exponent n is, dan is er een Fermat-drietal (a,b,c) bij exponent n met a en b relatief priem.
Bewijs. Stel dat (x,y,z) een Fermat-drietal bij exponent n is. Laat d de grootste gemene deler van x en y zijn. Wegens xn + yn = zn is dn een deler van zn. Hieruit volgt dat d een deler van z is. Stel a = x/d, b = y/d, c = z/d. Dan is (a,b,c) een Fermat-drietal bij exponent n met a en b relatief priem.
Stelling 2. Er is geen Fermat-drietal bij exponent 4.
Stelling 3. Er is geen Fermat-drietal bij exponent 3.
Stelling 4. Als er een Fermat-drietal bij exponent n > 4 is, dan is er een priemgetal p > 4 met een Fermat-drietal bij exponent p.
Bewijs. Neem zo'n Fermat-drietal (x, y, z) bij exponent n. Stel dat n geen macht van 2 is. Wegens n > 2, heeft n dan een deler p > 2 die een priemgetal is. Schrijf n = qp. Dan geldt (xq)p + (yq)p = (zq)p, zodat (xq,yq,zq) een Fermat-drietal voor exponent p is. Volgens Stelling 3 is p ongelijk 3. Omdat p een priemgetal is, volgt dat p > 4. Als n wel een macht van 2 is, dan kunnen we n = 4q schrijven. Op dezelfde manier als zonet blijkt dan dat (xq,yq,zq) een Fermat-drietal voor exponent 4 is, wat in strijd is met Stelling 2.
Stelling 5 (Gerhart Frey 1986, Jean Pierre Serre, 1987) Stel dat p een priemgetal is met p > 4 en dat (a,b,c) een Fermat-drietal is bij exponent p met a en b relatief priem en b even en a gelijk aan een viervoud plus 3. Dan is de kromme met de vergelijking: y2 = x(x-ap)(x+bp) elliptisch en semistabiel en opmerkelijk.
Het woord opmerkelijk is hier een afkorting van een stel eigenschappen van een bij de kromme horende tweedimensionale representatie van de Galois-groep van de het lichaam van de algebraische getallen. Zie [CSS] voor alle details.
Stelling 6 (Ribet, 1990) Een opmerkelijke elliptische kromme kan niet modulair zijn.
Stelling 7 (Wiles en Taylor, 1995) Elke semistabiele elliptische kromme is modulair.
Opmerking. Reeds vanaf 1967 wordt vermoed, dat elke elliptische kromme modulair is (Shimura, Taniyama, Weil). Wiles heeft dus een speciaal geval van dit vermoeden bewezen.
Samenvatting. Vanwege de stellingen 1, 2, 3, en 4 mogen we
aannemen, dat we een Fermat-drietal (a,b,c) hebben bij een exponent p >
4 die een priemgetal is, en dat a en b relatief priem zijn. Hieruit
volgt dat de getallen a en b zijn niet allebei even zijn. Als a en b
beide oneven zijn, is c even. Hieruit volgt dat precies één
van de
drie even is. Door de drie desgewenst te verwisselen en eventueel van
teken om te keren, kunnen we ervoor zorgen dat b even is, terwijl a en c
oneven zijn. Dan is a een viervoud plus 1 of een viervoud plus 3. Als
a een viervoud plus 1 is, kunnen we er een viervoud plus 3 van maken
door a, b, c door hun tegengestelden te vervangen. Stelling 5 levert
ons dan een opmerkelijke, semistabiele elliptische kromme
op. Deze kromme is volgens stelling 6 niet modulair en volgens stelling
7 wel. Dit is een tegenspraak. Dus Fermat-drietallen bestaan niet.
Dit bewijst het vermoeden van Fermat.
Terug naar de aspecten.
Het overkomt elke wiskundige wel dat hij een fout maakt in een bewijs. Het overkomt vele wiskundigen dat ze fouten vinden in gepubliceerde bewijzen van anderen. Men probeert dan ook voortdurend betere en inzichtelijker bewijzen te vinden voor belangrijke stellingen. Wijlen Van Lint uit Eindhoven zei anderzijds een keer: "Bewijzen controleren doe je liever niet. Een goed wiskundige voelt aan zijn water dat een stelling fout is."
De vraag is dus of we het bewijs van Wiles kunnen geloven, zie bv
[vdP] Lecture V. Op een conferentie in Boston in
1995, zie [CSS], hebben de knapste koppen uit de
wiskundige gemeenschap zich over Wiles' bewijs gebogen. Zij zijn tot
de conclusie gekomen dat het klopt, maar als ik [CSS] lees, kom ik voortdurend stappen tegen die ik
niet kan volgen. Ook de knapste koppen kunnen wel eens een steekje
laten vallen. Er is dus behoefte aan objectieve controle van
wiskundige bewijzen.
Terug naar de
aspecten.
Het met de computer controleren van wiskundige bewijzen is in Nederland begonnen in 1967 in het Automath project van N.G. de Bruijn, zie [NGdV]. Landau's leerboek "Grundlagen der Analyse" is geheel gecontroleerd in het proefschrift van L.S. van Benthem Jutting in 1977.
In het Computational Logic Project van R.S. Boyer en J S. Moore zijn met de stellingbewijzers THM en NQTHM onder meer de volgende stellingen bewezen: elk natuurlijk getal heeft op volgorde na precies een ontbinding als product van priemgetallen (1972), de kwadratische reciprociteitswet van Gauss (1984) en Goedels onvolledigheidsstelling (1986).
In 1973 startte het Mizar project met als doelstelling het formaliseren en per computer controleren van wiskunde.
Er zijn inmiddels computergecontroleerd bewijzen van de Stellingen 2 and 3, dwz. van Fermats vermoeden voor de exponenten 4 en 3. Deze zijn geleverd voor exponent 4 door Delahaye en Mayero gebruik makend van de stellingbewijzer Coq (zie [BeC]), en voor beide exponenten door Roelof Oosterhuis met de stellingbewijzer Isabelle.
Er zijn dus vrij veel verschillende stellingbewijzers, computerapplicaties waarmee wiskundige stellingen gecontroleerd zouden kunnen worden. Computercontrole van een wiskundig bewijs vergt allereerst een codering van de wiskundige theorie in een taal die de stellingbewijzer kan verwerken. Vervolgens wordt aan de stellingbewijzer duidelijk gemaakt hoe de stellingen uit de theorie bewezen worden. De stellingbewijzer kan dit namelijk bijna nooit zelfstandig, maar wel met hulp van een mens die inzicht heeft in het bewijs en de mogelijkheden van de stellingbewijzer.
Er zijn diverse kwaliteitscriteria voor stellingbewijzers. We noemen een stellingbewijzer "gezond" (sound) als je er geen onware beweringen mee kunt bewijzen. We noemen hem "intelligent" naarmate hij zelfstandiger in staat is om deelresultaten te controleren. Gebruikersvriendelijkheid is een ander criterium. Dit valt uiteen in enkele delen. Het is aan de ene kant van belang, dat de taal van de stellingbewijzer zoveel mogelijk lijkt op de gebruikelijke wiskundige taal. Het moet aan de andere kant ook relatief gemakkelijk zijn om de stellingbewijzer met correcte argumenten tot correcte gevolgtrekkingen te brengen ("hem te overtuigen"). Het is ook heel belangrijk dat de stellingbewijzer een duidelijke foutmelding geeft als hij een bepaalde stap in het bewijs niet kan volgen. Elke gezonde stellingbewijzer moet dit van tijd tot tijd melden, maar de helderheid van de melding is een zaak van gebruikersvriendelijkheid.
Elke stellingbewijzer heeft een typesysteem om hem in staat te stellen bv. gehele getallen te onderscheiden van andere wiskundige objecten zoals functies, breuken en oppervlakken. Een rijk typesysteem is nodig om ingewikkelde dingen uit te drukken. Stellingbewijzers met een rijk typesysteem hebben doorgaans minder ingebouwde intelligentie: hoe meer mogelijkheden je hebt, hoe moeilijker het wordt om daar intelligent mee om te springen. De stellingbewijzer NQTHM heeft een zeer arm typesysteem maar veel ingebouwde intelligentie. De stellingbewijzer PVS heeft een rijker typesysteem, is veel gebruikersvriendelijker dan NQTHM, maar had tot voor kort een release die niet gezond was.
Het typesysteem van NQTHM is niet rijk genoeg om de wiskunde nodig voor Wiles' bewijs van Fermats vermoeden op hanteerbare wijze uit te drukken. Vermoedelijk geldt dit ook voor PVS. De stellingbewijzers Coq en Mizar ken ik nog onvoldoende. Ik verwacht dat ze gezond zijn met een voldoend rijk typesysteem, maar met minder ingebouwde intelligentie dan PVS.
Verwar stellingbewijzers niet met computeralgebrapakketten zoals
Mathematica en Maple. Sinds de negentiger jaren gebruiken veel
wiskundigen dergelijke pakketten om hun formules te onderzoeken en
manipuleren. Deze bewerkingen vereisen dikwijls nevencondities die
door het pakket niet gecontroleerd kunnen worden. Het pakket op zich
biedt dus geen correctheidsgaranties. Het gebruik van een dergelijk
pakket in de computercontrole van een bewijs vergt dus de integratie
van het pakket in een stellingbewijzer. Ik denk dat de controle van
Wiles' bewijs van het Vermoeden van Fermat dit inderdaad nodig heeft.
Terug naar de aspecten.
Er kan in beginsel nog van alles mis gaan, hetzij bij het coderen van de theorie, hetzij doordat de stellingbewijzer niet gezond blijkt te zijn. Computercontrole van wiskundige bewijzen is dus in beginsel niet meer dan een grote versterking van het subjectieve mechanisme van controle van het bewijs door de gemeenschap van wiskundigen.
Menselijke verificatie zal altijd nodig blijven om te zien of de betreffende theorie correct ingevoerd is. Menselijke controle is echter goed mogelijk als de taal van de stellingbewijzer redelijk leesbaar is. Het punt van de gezondheid is minder problematisch. Een ongezonde release van een stellingbewijzer is namelijk geen lang leven beschoren en het onopvallend gebruik maken van de ongezondheid van een stellingbewijzer is moeilijk en riskant.
Er is ook een fundamentelere methode om het gezondheidsprobleem
aan te pakken. Een stellingbewijzer zou in beginsel bij elk bewijs een
certificaat op moeten leveren. Dit is een bestand of een stel
bestanden, dat de bewezen bewering bevat tezamen met alle gebruikte
definities en axioma's en een "getuige" van het bewijs die door een
zg. certificator geverifieerd kan worden. Een certificator is veel
eenvoudiger dan een stellingbewijzer. Het heeft geen intelligentie of
gebruikersvriendelijkheid nodig. Zijn correctheid is dus veel
eenvoudiger na te gaan. Integratie van een computeralgebrapakket in de
stellingbewijzer zal echter vermoedelijk problemen geven voor de
certificaten of de certificatoren.
Terug naar de aspecten.
De aandachtspunten, die in het vorige aspect genoemd zijn, zijn zeker
oplosbaar. Mijn antwoord op deze vraag is dus een volmondig ja.
Terug naar de aspecten.
Controle door middel van een computerprogramma vereist het gebruik van een stellingbewijzer voor het hele project. De talen van verschillende stellingbewijzers hebben namelijk talloze, soms heel subtiele betekenisverschillen, zodat overdracht van resultaten tussen verschillende stellingbewijzers lastig en riskant is. We hebben dus een stellingbewijzer nodig die het hele project kan ondersteunen. Dit vergt een rijk typesysteem en vermoedelijk ook een in de stellingbewijzer geïntegreerd computeralgebra-pakket. Voorzover ik weet is een dergelijke stellingbewijzer nog niet beschikbaar.
Ik denk echter wel dat het project uitvoerbaar is, en zelfs dat het in (laten we zeggen) vijftig jaar inderdaad uitgevoerd zal worden. Het is beslist niet binnen handbereik. Het project is qua omvang vergelijkbaar met het werk van Bourbaki. Tussen 1950 en 1980 heeft een van oorsprong Franse groep wiskundigen een nieuwe formele basis voor grote stukken van de zuivere wiskunde gelegd, wat gepubliceerd is in een twintigtal boeken onder het pseudoniem N. Bourbaki.
Het voorliggende Fermat-Wiles project zou geadopteerd kunnen worden door de Mizar groep. Deze groep is al 32 jaar actief en heeft een groot aantal stukjes wiskunde geformaliseerd. Mijn indruk is vooralsnog dat de groep te klein is en te weinig focus heeft om echt zoden aan de dijk te kunnen zetten. Ik moet dit echter nog nader bestuderen.
Een vrijblijvende fantasie. Als ik het project zou moeten uitvoeren, zou ik eerst de grenzen van het typesysteem willen uittesten door het formaliseren van de eerste tien bladzijden van [EGA1]. Dit behelst een bewijs van Yoneda's Lemma voor grote categorieën. Yoneda's Lemma zelf is al in Mizar en Coq geformaliseerd, maar ik weet nog niet hoe het zit met toepasbaarheid op grote categorieën. Ik ga niet zelf een stellingbewijzer met geïntegreerd computeralgebrapakket bouwen. Toch zou het volgende deel van het project moeten bestaan uit de behandeling van complexe functietheorie en modulaire vormen, in het bijzonder Weierstrass p-functie en Eisenstein reeksen. Na deze voorbereidingen is het tijd voor elliptische krommen over de rationale getallen met goede en slechte reductie, en de werking van de Galois groep op het Tate moduul. Dit alles zou in tien jaar bereikbaar moeten zijn. Het is echter niet meer dan een bescheiden begin. Hebben we Deligne's bewijs van de Weil vermoedens nodig?....
Het project vergt dus een monnikenwerk geheel in de lijn van de
zinspreuk van het
Koninklijk Wiskundig Genootschap
"Een onvermoeide arbeid komt alles te boven".
Terug naar de aspecten.
Je zou tot dit project iedereen kunnen rekenen die werkt aan de
formalisatie van wiskunde of aan het bouwen en verbeteren van
stellingbewijzers en computeralgebrapakketten. Wereldwijd gaat het dan
om vrij veel mensen. Wanneer we ons echter beperken tot de
computercontrole van Wiles' bewijs van de Stelling van Fermat,
is het antwoord, dat niemand daaraan werkt omdat we nog lang niet zover
zijn.
Terug naar de aspecten.
Als gezegd, het formaliseren en met computers controleren van wiskunde begon in Nederland in 1967 in het Automath project van N.G. de Bruijn, cf. [NGdV]. Landau's "Grundlagen der Analyse" werd volledig gecontroleerd in het proefschrift van L.S. van Benthem Jutting in 1977. Tegenwoordig is het werk aan formalisatie van de wiskunde vooral geconcentreerd in Nijmegen, zie de webpagina's van Barendregt en Geuvers.
Een verwant gebied is de computercontrole van de correctheid van
computer programma's en algoritmen. Dit is niet in Nederland begonnen,
maar er is hier veel aan gedaan. Zo zijn er tenminste vier proefschriften
aan gewijd, die van Wishnu Prasetya (Utrecht, 1995), Tanja Vos (Utrecht,
2000), Marieke Huisman (Nijmegen, 2001) en Gao Hui (Groningen, 2005), zie
bv. de webpagina's van
Swierstra
(Utrecht), Jacobs (Nijmegen) en
mij zelf
(Groningen).
Terug naar de aspecten.
Het vermoeden van Fermat is onderdeel van de getaltheorie. Door het werk van Frey, Serre en Ribet is het probleem overgebracht naar de algebraische meetkunde en de analyse (elliptische krommen en modulaire vormen). Het bewijs van Wiles hoort daar thuis. De computercontrole van wiskundige bewijzen behoort tot de computationele logica, een nieuw vakgebied ergens tussen de wiskundige logica en de informatica. De eerder genoemde computeralgebrapakketten horen tot het gebied van de computeralgebra, dat ook ergens tussen wiskunde en informatica inhangt.
Wiles' bewijs berust op een groot aantal resultaten uit verschillende
takken van de wiskunde. Computercontrole zou dus baat kunnen hebben van
semantische databases. De totale hoeveelheid kennis die geformaliseerd
moet worden is gigantisch. Het project kan dus beschouwd worden als een
oefening in software engineering, refactoring van de helft van
de zuivere wiskunde. Kennissystemen, databases en software engineering
zijn takken van de informatica. Toch ben ik geneigd om het probleem als
een wiskundeprobleem te zien. Wiskundigen vinden het in het algemeen
echter belangrijker nieuwe wiskunde te ontwikkelen dan "oude wiskunde"
vast te leggen en te controleren.
Terug naar de aspecten.
Het is goed mogelijk dat er ooit een eenvoudiger bewijs gevonden zal worden. Dat is echter een uitdaging voor de wiskundigen en niet voor de informatici. Mocht het gebeuren, dan is er natuurlijk reden om dat eenvoudiger bewijs eerst te behandelen.
Wat mij betreft, gaat het in Bergstra's probleem echter om het
formaliseren en controleren van de stelling van Wiles, dat elke
semistabiele elliptische kromme modulair is. Dit vergt het
formaliseren van grote delen van de theorieen van de elliptische
krommen en van de modulaire krommen. Uiteraard zullen de wiskundigen
ook dit bewijs zo net mogelijk proberen te maken. Of dat essentiele
vereenvoudigingen op zal leveren, staat te bezien.
Terug naar de aspecten.
Eigenlijk wel. Dit is echter een nog grotere uitdaging en dan
eerder voor het vakgebied kunstmatige intelligentie dan voor
informatica zelf.
Terug naar de aspecten.
Zie desgewenst mijn start pagina. Ik ben
in 1975 gepromoveerd op een proefschrift in de algebraische meetkunde
(singulariteiten en werkingen van lineaire algebraische groepen). In
de tachtiger jaren ontwikkelde ik een soort computeralgebra
programma's voor de klassificatie van bovendriehoeksmatrices. Ik ben
toen overgestapt naar de informatica, in eerste instantie semantiek
van programmeertalen, later formele methoden ten behoeve van
concurrentie. Rond 1992 ben ik begonnen de stellingbewijzer NQTHM te
gebruiken ter ondersteuning van correctheidsbewijzen van concurrent
algoritmen. Ik werk sinds 2003 met de stellingbewijzer PVS, onder meer
voor het ontwikkelen van een verfijningstheorie voor concurrent
algoritmen. Ik ben dus geen specialist op het gebied van dit virtuele
project, maar ik heb ervaring in diverse gerelateerde gebieden.
Terug naar het begin.
Ik streef niet naar volledigheid, maar ik wil deze pagina wel zo leesbaar, representatief, correct en evenwichtig mogelijk maken. Alle vragen, correcties en opmerkingen zijn daarom welkom.