Je leest:

Blokken stapelen is geen kinderspel

Blokken stapelen is geen kinderspel

Auteur: | 1 februari 2011

In 1985 werd door twee wiskundigen een vermoeden geformuleerd over het symmetrisch stapelen van blokken. Een kwart eeuw later is er een bewijs. Computerrekenwerk was hierbij onmisbaar: uitgeschreven zouden alle berekeningen meer dan een miljoen volgedrukte A4-tjes in beslag nemen.

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.

Computerbewijzen

Een computer kan berekeningen uitvoeren, maar tegenwoordig wordt er ook veel onderzoek gedaan naar automatische stellingen-bewijzers. Hierbij gaat de computer een stap verder: hij levert automatisch bewijzen. De gebruiker geeft het programma een uitspraak, en het systeem probeert hier automatisch een bewijs voor te vinden.

Er is een hele industrie van dit soort programma’s, die allemaal proberen om zoveel mogelijk uitspraken automatisch te kunnen bewijzen. Manuel Kauers, Christoph Koutschan en Doron Zeilberger zijn ervan overtuigd dat voor een bepaald type wiskundige problemen de toekomst in computerbewijzen ligt.

Ook in Nederland wordt op dit terrein veel onderzoek gedaan aan de Radboud Universiteit in Nijmegen. Zie bijvoorbeeld De kunst van het bewijzen (pdf) van Freek Wiedijk over dit onderwerp.

Zie ook:

Dit artikel is een publicatie van NEMO Kennislink.
© NEMO Kennislink, sommige rechten voorbehouden
Dit artikel publiceerde NEMO Kennislink op 01 februari 2011

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.