Wiskundemeisjes

De favoriete (nog levende!) wiskundige van... (7)

Georges Gonthier

Georges Gonthier is onderzoeker bij Microsoft Research. Hij zoekt manieren om de werking van computerprogramma's formeel te controleren. Iemand kan namelijk wel beweren dat een bepaald computerprogramma iets bepaalds doet, maar je wil ook kunnen aantonen dat zo'n programma inderdaad doet wat het belooft. Vaak gaat dat weer met behulp van een computer.Gonthier heeft samen met Benjamin Werner een formeel computerbewijs van de beroemde vierkleurenstelling gemaakt dat helemaal gecontroleerd is. Daarvoor gebruikte hij Coq, een proof assistent (bewijsassistent). Dat is een computersysteem dat je kunt gebruiken om formele bewijzen te controleren.

Gonthier vindt zichzelf eigenlijk geen wiskundige maar informaticus, maar zijn onderzoek heeft zoveel met wiskunde te maken dat hij toch zijn favoriete wiskundige mag noemen. Na enig nadenken noemt hij John Conway (1937) zijn favoriete nog levende wiskundige.

John Conway
Zoals het een beroemd wiskundige betaamt, bestaan er leuke anekdotes uit Conways jeugd. Toen hij vier was, kon hij machten van twee opdreunen. En toen hij op zijn elfde ondervraagd werd voor hij naar de middelbare school ging antwoordde hij op de vraag wat hij later wilde worden: "Wiskundige op Cambridge!"

Dat lukte inderdaad, in 1964 kreeg hij daar een aanstelling. Hij werkte daar eerst aan logica, maar het ging niet zo goed met hem. Hij had het gevoel dat hij geen "echte" wiskunde aan het doen was, had nog niets gepubliceerd en voelde zich daar erg schuldig over. Maar toen kwam de grote doorbraak. Rond 1965 vond John Leech een dichte bolpakking in dimensie 24. (In hogere dimensies dan 3 kun je ook definiëren wat bollen zijn en bekijken hoe ze zó kunnen worden gestapeld dat er zo weinig mogelijk ruimte open blijft.) Bij die bolpakking hoort een rooster, het Leech rooster. Leech wilde de symmetrieën van dit rooster beter begrijpen. Daarom zocht hij iemand met meer verstand van symmetriegroepen dan hij zelf had, en Conway was de eerste die interesse toonde. Conway vond de symmetriegroep van het Leech rooster en dit bleek een heel bijzondere groep te zijn, die nog niet bekend was.

In 1970 werd Conway ook bekend bij een groter publiek, toen hij zijn beroemde game of life ontwikkelde. Dat werd meteen een groot succes. Denk aan een oneindig groot ruitjespapier. Breng een aantal vakjes tot leven, door ze te kleuren. Nu gebeurt er in elke stap het volgende:

voor een levend (gekleurd) vakje:
als het vakje geen of maar één levend buurvakje heeft, gaat het dood (uit eenzaamheid)
als het vakje vier of meer levende buurvakjes heeft, gaat het dood (door overbevolking)
als het vakje twee of drie buren heeft blijft het leven

voor een dood (wit) vakje:
als het vakje drie levende buren heeft, wordt het levend

Een animatie van het spel kun je vinden op deze website.

Conway is ook beroemd vanwege zijn ontdekking van de surreële getallen en zijn werk in knopentheorie, getaltheorie, speltheorie, kwadratische vormen, coderingstheorie en betegelingen.

Gonthier kiest voor Conway omdat die naam steeds opduikt als hij zelf aan een nieuw onderwerp gaat werken. Toen hij bijvoorbeeld begon te lezen over groepentheorie en formele logica, toen bleek dat Conway in die twee gebieden al van alles had gedaan. Gonthier is onder de indruk van Conways surreële getallen en roemt zijn inzicht gevende werken. Conway lijkt structuur te kunnen plukken uit het niets!

(Jeanine)