Je leest:

Bewijzen met computers

Bewijzen met computers

Auteur: | 29 oktober 2012

Een oud wiskundig bewijs is nu opnieuw uitgevoerd door wetenschappers van Microsoft Research. Interessant, omdat het bewijs dat ze nu hebben gegeven volledig met een computer gecontroleerd kan worden.

De stelling van Feit-Thompson is bewezen. Alweer, nadat het bijna 50 jaar terug al gedaan was. Waarom zou je iets een tweede keer bewijzen? Omdat een computer het nieuwe bewijs kan checken. Zes jaar heeft het geduurd voordat Georges Gonthier en zijn collega’s eindelijk hun einddoel bereikten. Een formeel, controleerbaar bewijs van de stelling van Feit-Thompson, een belangrijke stelling uit de groepentheorie. Gonthier is er dolblij mee. “Dit is echt het Einde”, schrijft hij in een email aan zijn collega’s.

Dit bewijs komt geeneens in de buurt van het langste wiskundige bewijs ooit.

Wat ze precies hebben bewezen? De stelling van Feit-Thompson zegt dat ‘elke eindige groep met oneven orde oplosbaar is’. Dit betekent dat een wiskundige groep met een eindig, oneven aantal elementen te creëren is door een aantal Abelse groepen uit te breiden. Een erg ingewikkelde stelling (zie voor een kleine introductie van groepentheorie het kader), ook al is hij met eenvoudige woorden op te schrijven.

Wat is groepentheorie?

De groepentheorie waar deze stelling in thuishoort is een ingewikkeld onderdeel van de algebra. In de wiskunde is een groep een verzameling objecten waar een bewerking bij hoort en die aan bepaalde eisen voldoet. Deze eisen zijn geslotenheid, associativiteit, identiteit en inverteerbaarheid.

De Rubiks kubus is een mooi voorbeeld van een wiskundige groep.

Een mooi voorbeeld van een groep is een Rubiks kubus, met de draaiing van de kubus als bewerking. Hoe je de kubus ook draait, het is nog steeds dezelfde vorm (geslotenheid). Twee keer naar rechts draaien aan de kubus en daarna een derde draai naar boven is natuurlijk hetzelfde als een keer naar rechts draaien en daarna een keer naar rechts en een keer naar boven (associativiteit).

De kubus niet draaien is de identiteit, en de kubus een keer draaien en vervolgens in de tegenovergestelde richting nog een keer draaien is een inverse bewerking.

De Rubiks is dus een groep. Het is echter geen Abelse groep; daarvoor zou bijvoorbeeld een draai naar links en een draai naarboven dezelfde kubus moeten opleveren als een draai naar boven en dan een draai naar links, en dat is niet zo (deze eis heet commutativiteit).

Het mag duidelijk zijn dat een groep een vrij ingewikkeld ding is. Toch komen ze overal in de wiskunde voor. De gehele getallen zijn bijvoorbeeld een groep met de bewerking optellen. Ook in de cyberwereld zijn groepen belangrijk; zonder groepentheorie zouden er nooit goede encryptiemethoden zijn, waarmee bijvoorbeeld betalingen via internet worden beveiligd.

Meer over groepentheorie is onder andere in dit artikel te lezen.

Een formeel bewijs is een bewijs dat uit een eindig aantal vastomlijnde stappen bestaat. Het voordeel van zo’n bewijs, ten opzichte van andere bewijzen, is dat het makkelijk te programmeren is. Beter nog, een formeel bewijs is ook eenvoudig te controleren met behulp van een computer. Als een wiskundig bewijs heel erg groot wordt, zoals bijvoorbeeld het bewijs van de laatste stelling van Fermat, kan het heel moeilijk zijn om met de hand na te gaan of het klopt. Door een bewijs formeel op te schrijven, kan het checken aan een computer overgelaten worden, en weet je zo sneller of je bewijs klopt of niet.

Lang bewijs

Varianten van het probleem waren al langer bekend voor 1963. Maar Feit en Thompson schreven voor het eerst het bewijs van de stelling op. Het bleek nogal een bewijs te zijn: hun versie omvatte maar liefst 255 pagina’s en werd in twee boekwerken uitgebracht. In die tijd gold dit bewijs als een doorbraak; nog nooit was er in de groepentheorie een bewijs dat meer dan een paar pagina’s lang was verschenen.

Sinds het bewijs van Feit en Thompson zijn er meer van dergelijke superbewijzen verschenen, maar zij waren de eerste. In 1963 waren er nog geen computers waarmee je de ingewikkelde dingen misschien snel kon berekenen, dus Feit en Thompson hebben alle 255 pagina’s van het bewijs stukje voor stukje met de hand ontdekt.

Computerwiskunde

Het is dan ook geen verrassing dat het bewijs dat nu is verschenen van Gonthier zes jaar nodig had om gemaakt te worden. Een groot verschil met vroeger is dat er nu wel computers zijn. Nog niet precies om het zware werk voor de wiskundigen te doen, maar om het te controleren.

Georges Gonthier.

“Omdat dit bewijs met de computer gecontroleerd kan worden, kunnen we meer informatie eruit halen. We weten dat het absoluut klopt”, zegt Gonthier op de site van Microsoft Research, waarbij hij in dienst is. Hij ziet de toekomst van computers als ‘echte wiskundigen’ in plaats van ‘veredelde rekenmachines’ rooskleurig in. “We wilden door dit bewijs te formaliseren vooral onderzoeken of je met computers ook echt wiskunde kan doen. Niet het berekenen van sommen, maar het echt nadenken over waarom een som op een bepaalde manier berekend wordt. Ik denk dat dit project laat zien dat dat kan.” Gothier is trouwens geen vreemde op het gebied van het formaliseren van bewijzen. Eerder loste hij al het vierkleurenprobleem op formele wijze op.

Het idee dat een computer een bewijs kan verifieren, is al langer bekend en wordt ook al gebruikt. Of een computer straks ook, uit zichzelf, een bewijs kan maken, dat zal nog moeten blijken. Het zou de wiskundigen in ieder geval veel (soms saai en tijdrovend) werk uit handen nemen.

Lees meer op Kennislink over bewijzen met de computer:

Oeps: Onbekende tag `feed’ met attributen {"url"=>"https://www.nemokennislink.nl/kernwoorden/computerbewijs/index.atom", “max”=>"5", “detail”=>"minder"}

Dit artikel is een publicatie van NEMO Kennislink.
© NEMO Kennislink, sommige rechten voorbehouden
Dit artikel publiceerde NEMO Kennislink op 29 oktober 2012

Discussieer mee

0

Vragen, opmerkingen of bijdragen over dit artikel of het onderwerp? Neem deel aan de discussie.

NEMO Kennislink nieuwsbrief
Ontvang elke week onze nieuwsbrief met het laatste nieuws uit de wetenschap.