Een project is erop gericht om computers te leren wiskundige stellingen te bewijzen, wat voor hen bijzonder moeilijk is. âIk heb een echt bewonderenswaardig bewijs gevonden, maar de kantlijn van het boek is te klein om het erin te zettenâ. Dit schreef de 17e-eeuwse Franse wiskundige Pierre de Fermat toen hij zijn âlaatste stellingâ poneerde. Het duurde drie decennia voordat het laatste probleem van Fermat werd teruggevonden tussen de papieren van de wiskundige en nog eens drie eeuwen voordat dat bewonderenswaardige bewijs werd ontdekt.
En toch is de zaak nog niet helemaal opgelost, alleen de uitdaging is iets anders.
Het aan een computer laten zien. De nieuwe uitdaging is om een computer de ongrijpbare stelling te laten bewijzen. Dat is het doel van een nieuw project, Formalising Fermat, geleid door het Imperial College in Londen.
Het probleem van Fermat. De âlaatste stellingâ van Fermat stelt dat, als a, b en c natuurlijke getallen zijn en niet gelijk aan nul, de vergelijking a^n+b^n=c^n geen oplossing heeft als n groter is dan twee. Iets formeel bewijzen is niet zo eenvoudig als het met vallen en opstaan bewijzen, en dit bewijs, te complex voor de âmagere margeâ van Fermats notitieboekje, zou eeuwenlang verloren gaan.
Het probleem werd in 1994 opgelost door de Brit Andrew Wiles, die al op 10-jarige leeftijd begon met het oplossen van deze puzzel. In 2016 kreeg Wiles de Abelprijs, de âNobelprijs voor de wiskundeâ.
Bijna een miljoen pond. Nog eens 30 jaar nadat het enigma was opgelost en meer dan drie eeuwen na de dood van Fermat, heeft een team van onderzoekers, onder leiding van Kevin Buzzard van het Imperial College in Londen, een andere stap genomen door een computer te leren het probleem op te lossen.
Het nieuwe project ging eind 2024 van start en loopt tot 2029. Het heeft een financiering van iets meer dan 934.000 pond en begint al wat resultaten op te leveren, in de vorm van stukjes code die worden toegevoegd aan een database op GitHub.
Hetlijkt misschien contra-intuĂŻtief, maar dit soort redeneren, het soort redeneren dat ons in staat stelt om formeel wiskundige stellingen te bewijzen, is moeilijk om computers te leren.
Onlangs legden Buzzard en andere experts de complexiteit van de kwestie uit aan de Franse krant Le Monde. Om te beginnen moeten we in gedachten houden dat de oplossing van deze stelling complex is, en het is geen toeval dat verschillende generaties wiskundigen hun hersens hebben gepijnigd om hem te vinden.
Deze wiskundigen hadden ook eerdere ervaring op het gebied van het oplossen van dit soort problemen. Zoals Buzzard uitlegde aan de Franse krant, hebben wiskundigen een basis die hen in staat stelt om âstappen over te slaanâ als het gaat om het uitleggen van de oplossing van dit probleem. Een computer moet echter helemaal opnieuw beginnen als het aankomt op het construeren van zijn eigen verklaring voor het probleem.
De laatste stelling van Fermat (…) heeft geen toepassingen in de echte wereld, noch theoretisch, noch praktisch,â vertelde Buzzard een paar maanden geleden aan het tijdschrift New Scientist. Dus waarom al deze moeite om een computer te leren iets op te lossen dat we al hebben opgelost? De sleutel ligt hier niet in het verleden maar in de toekomst.
Zoals het team achter het project uitlegt, kunnen computers tegenwoordig worden gebruikt om wiskundigen te helpen bij het oplossen van problemen zoals het bewijzen van stellingen, maar er is een obstakel voor het realiseren van sommige vormen van hulp.
Het probleem, zo geven ze aan, is dat weinig wiskundigen zich hebben toegelegd op het werken met deze software, waardoor er geen hulpmiddelen zijn die de âdefinitiesâ hebben die wiskundigen gebruiken om deze problemen op te lossen. Het werk aan dit probleem moet dienen om de databases te creĂ«ren die nodig zijn om soortgelijke problemen in de toekomst op te lossen.
