Wiskundigen spelen ook met blokken. Niet voor de lol, maar bloedserieus onderzoek. Het gaat om de vraag hoeveel stapelingen er onder bepaalde voorwaarden mogelijk zijn. Het uitgangspunt is een vierkant oppervlak dat onderverdeeld is in kleinere vierkantjes van gelijke grootte, zoals een schaak- of dambord. De regels: een stapel blokken mag niet hoger zijn dan het aantal vierkantjes langs de zijde van het oppervlak (bij een schaakbord 8, bij een dambord 10), en ook niet hoger dan een stapel blokken achter of links van de stapel.

Het aantal mogelijkheden om onder deze voorwaarden de blokken te stapelen, is makkelijk uit te rekenen, althans, voor wiskundigen. Zie bijvoorbeeld het Wikipedia-lemma of het Wolfram MathWorld-lemma over plane partitions. Knap lastiger wordt de vraag als de blokkenstapels bovendien aan bepaalde symmetrie-eisen moeten voldoen. In de afgelopen decennia werden al formules opgesteld waarmee deze vraag beantwoord kan worden. Van geen van die formules was de juistheid echter bewezen. Het waren vermoedens en niet meer dan dat.

Het aantal mogelijkheden om blokken zó te stapelen dat er sprake is van ‘volmaakte symmetrie’ kan eindelijk berekend worden dankzij vernuftig gebruik van de computer. Dit plaatje geeft een volmaakt symmetrische plane partition op een veld van 7 bij 7.

Manuel Kauers, Christoph Koutschan en Doron Zeilberger

Een van die formules berekent het aantal mogelijke stapelingen waarbij er sprake is van ‘volmaakte symmetrie’. De correctheid van die formule, in de jaren 1980 opgesteld door George Andrews en David Robbins, is nu bewezen door Christoph Koutschan en Manuel Kauers van het Research Institute for Symbolic Computation van de
 Johannes Kepler Universität in Linz, Oostenrijk. Zij werkten samen met professor Doron Zeilberger van Rutgers, State University of New Jersey (Verenigde Staten).

Manuel Kauers, Christoph Koutschan en Doron Zeilberger zijn ervan overtuigd dat voor een bepaald type wiskundige problemen de toekomst in computerbewijzen ligt.

Koutschan: “We lieten de computer het werk doen!” Het klinkt misschien eenvoudig: je stopt een paar gegevens in een computer, past een paar beperkende voorwaarden aan en gaat koffie drinken terwijl de computer rekent. Niets is echter minder waar: “De belangrijkste stap was om het Andrews-Robbins-vermoeden te vertalen in een geschikte vorm zodat de computer in staat is het bewijs te leveren”, verklaart Koutschan.

Een miljoen pagina’s tellend bewijs

Met het bewijs van het Andrews-Robbins-vermoeden hebben de twee Oostenrijkers en de Amerikaan het laatste gat gedicht van een reeks open problemen die in 1985 werden gepresenteerd tijdens een conferentie in Montreal. In de daaropvolgende jaren werd het ene na het andere vermoeden van die lijst bewezen. Maar het Andrews-Robbins-vermoeden bleek erg hardnekkig.

“Dit probleem bleef bijna dertig jaar lang onopgelost. Het bewijs werd uiteindelijk ‘automatisch bewezen’, wat aangeeft dat moderne computerprogramma’s in staat zijn om iets te kraken wat ons mensen niet lukt”, aldus Kauers. Het resultaat van de computer, die ‘slechts een paar maanden’ nodig had om de klus te klaren, zou op papier een miljoen A4-pagina’s omvatten. Het handwerk van de onderzoekers is bescheidener van omvang: hun artikel, dat zal verschijnen in het vaktijdschrift Proceedings of the National Academy of Sciences, neemt niet meer dan vier pagina’s in beslag.

Zie ook:

• A proof of George Andrews’ and David Robbins’ q-TSPP conjecture (Engels, pdf, technisch!)
• Formele bewijzen: het DNA van de wiskunde (Kennislinkartikel)
• Laatste twijfels vierkleurenprobleem weggewerkt (Kennislinkartikel)
• Computer stapelt sinaasappels (Kennislinkartikel)
• Artikel van Bennie Mols over computerbewijzen (pdf, NRC Handelsblad)
• De kunst van het bewijzen (pdf)