Er is weer een oud wiskundeprobleem opgelost, maar er is één probleem: de redenering en het bewijs controleren kost zoveel rekenwerk dat de uitkomst nooit door mensen te checken is. Het bewijs is met een computer gemaakt en kan nu dus ook alleen door een computer gecontroleerd worden… Geldt het dan wel?
Een oud probleem van de excentrieke wiskundige Paul Erdös is gedeeltelijk opgelost. Erdös bedacht zijn zogenoemde Erdös-discrepantieprobleem in de jaren ’30 en beloofde 500 dollar aan degene die het op kon lossen. Het probleem ging over een rij van eentjes met afwisselend een plusje of een minnetje ervoor: +1, -1, +1, -1, +1, -1, enzovoort…
De vraag was of er altijd een specifiek stukje van de rij te kiezen is, zodat de absolute som van dat stukje groter is dan C, waarbij C elk getal mag zijn dat je wilt.
Neem bijvoorbeeld de deelrij -1 -1 -1 -1 +1 +1 -1 -1 -1. Alles bij elkaar optellen van links naar rechts levert dan in absolute waarde het getal 5 op. Eerder bewees men al een onderdeel van dit bewijs: er is altijd een deelrij met twaalf eentjes of meer erin, waarbij de optelsom groter of gelijk is aan één. De vraag is nu: bestaat er een dergelijke rij voor élk getal?
Die vraag is moeilijk te beantwoorden, omdat je steeds meer moet checken; een rijtje van 12 ééntjes samenstellen zo dat de netto som groter dan 1 is, is nog wel te doen. Maar als je een rij zoekt waarbij het verschil groter dan 2 moet zijn, komen er steeds meer opties. Al snel werd duidelijk dat het menselijk rekenvermorgen niet voldoende zou zijn.
Groter dan wikipedia
Daarop besloten wiskundigen van de universiteit van Liverpool om een computer te gebruiken. Die heeft immers geen enkele moeite met veel rekenwerk. Met een slim programma kon de computer alle mogelijkheden voor getallenrijtjes afgaan en berekende zo de minimale lengte van een rijtje met een totaalverschil van 2 en kwam op 1161. Aanzienlijk meer dan de 12 voor een verschil van 1, en dat liet zich ook zien in het rekenbewijs: dat was 12 gigabyte groot. Ter vergelijking: Wikipedia, de website met nagenoeg alle kennis die mensen hebben, bevat slechts 10 gigabyte aan tekst. Daarmee is dit bewijs ook verreweg het grootste in de wiskundewereld; vorige reuzenbewijzen waren hooguit 1000 á 2000 pagina’s lang.
Met een bewijs dat groter is dan het aantal pagina’s van wikipedia kan je behoorlijk wat schoolborden volschrijven met ondoordringbare formule’s.
Flickr.com, Mike Scoltock via CC BY-NC 2.0Of dit bewijs telt is echter nog maar de vraag. De tekst is immers geen menselijke wiskundige redenering; het is ‘slechts’ een computerberekening op papier. Daarnaast doet zich een ander probleem voor: niemand heeft de tijd om dit bewijs te checken. Daarmee lijkt bijna een nieuwe tijd aangebroken in de wiskunde, waarbij computers dusdanig overdadige berekeningen maken dat ze niet meer door mensen te checken zijn; en daarmee misschien wel niet legitiem zijn.
Logica-bewijs
Aan de andere kant worden ook op dit moment wiskundige bewijzen af en toe met de computer gecheckt. Vooral logica-bewijzen, die enkel en alleen uit van te voren omschreven stappen bestaan om zo iets nieuws af te leiden, zijn goed door een computer op correctheid te checken; voer immers de mogelijke stappen in en de computer kijkt of er niet gesjoemeld is.
Daarnaast zijn voor getaltheoretische stellingen computers vaak een uitkomst om een idee te geven over de juistheid. Zo vermoedde men dat het tweelingpriemvermoeden – er zijn oneindig veel tweelingpriemen die maar 2 van elkaar verschillen – waar was, doordat men zelfs bij zeer grote getallen met een computer priemparen vond. Natuurlijk is dat nooit een écht bewijs… Als iets de eerste zes miljard keer klopt, hoeft het niet de zes miljard-en-eerste keer ook zo te zijn; in ieder geval niet in de wiskunde.
Existentie
Dat een computer bij dit verhaal wel uitkomst biedt, komt doordat het hier gaat om een existentiebewijs; de computer toont aan dát iets kan, niet dat het áltijd kan. Aantonen dat iets kan is in dit geval een kwestie van alle mogelijke deelrijtjes van een bepaalde lengte checken. Dat is veel werk (een rijtje van 1161 heeft 2 1161 mogelijke volgordes) maar voor een computer wel te doen.
Misschien is het wel geruststellend dat zelfs de computer niet de hele Erdös-stelling niet kan bewijzen; die zegt immers dat je een willekeurig groot verschil kan vinden in een bepaalde deelrij; tot nu toe is er alleen bewijs voor een verschil van 1 of 2. De uitbreiding naar een algemeen bewijs zal, naar alle waarschijnlijkheid, toch nog op menselijk vernuft aankomen en niet op zuivere rekenkracht.