Het artikel bespreekt de oplossing van de Vierkleurenstelling in 1976 door Kenneth Appel en Wolfgang Haken. De doorbraak was controversieel omdat een groot deel van het bewijs werd geleverd door een computer, wat leidde tot een fel debat over de validiteit van bewijzen die te omvangrijk zijn voor menselijke verificatie.
Belangrijke punten uit het artikel:
- Verzet: Veel wiskundigen wezen het bewijs af omdat het volgens hen geen 'wiskundige redenering' bevatte, maar steunde op een 'Orakel'.
- Generatiekloof: Er was een duidelijk verschil in acceptatie; oudere wiskundigen vertrouwden de computer niet, terwijl jongere wiskundigen geen vertrouwen hadden in handmatige berekeningen van honderden pagina's.
- Filosofie: De discussie verschoof naar de vraag of computerondersteunde bewijzen een legitieme uitbreiding zijn van traditionele methoden, waarbij wordt betoogd dat computers, in tegenstelling tot mensen, niet moe worden en minder foutgevoelig zijn.
- Impact: Dit moment wordt gezien als het begin van een nieuw tijdperk in de wiskunde, waarbij machines een essentiële rol gingen spelen in complexe bewijsvoering.
De eerste keer dat machines wiskundigen overtroffen
In juli 1976 werd een wiskundig mysterie dat wiskundigen al meer dan een eeuw verbijsterde eindelijk opgelost: de Vierkleurenstelling.
Definitie: Vierkleurenstelling De Vierkleurenstelling stelt dat er niet meer dan vier kleuren nodig zijn om de regio's van elke willekeurige kaart zo in te kleuren dat geen twee aangrenzende regio's dezelfde kleur hebben.
De auteurs — Kenneth Appel en Wolfgang Haken — schreven het succes toe aan een onconventionele collaborator: een computer had een groot deel van het zware wiskundige werk verricht, om precies te zijn 1.200 uur rekentijd en 10 miljard beslissingen. De computerprogrammeur John Koch hielp Appel en Haken bij het algoritmische werk.
Appel en Haken zouden later beschrijven hoe het systeem hen "dingen begon te leren over hoe we verder moesten gaan die we nooit hadden verwacht", waarbij ze toegaven dat het systeem de makers op bepaalde intellectuele taken was "ontstegen". Een nieuwe wereld van mens-machine-wiskunde was begonnen, wat de vraag opriep: kunnen we vertrouwen op een wiskundig bewijs dat te omvangrijk is voor een mens om te verifiëren?
Ontvangst
De reacties van wiskundigen varieerden van acceptatie tot afwijzing en zelfs ontkenning, in plaats van universele bewondering. Wiskundigen, die trots zijn op hun rationaliteit, werden plotseling geconfronteerd met een wiskundige 'moloch' in wat moet hebben gevoeld als religieuze ketterij.
"God zou niet toelaten dat de stelling werd bewezen door een methode die zo verschrikkelijk is!" — Herbert Wilf, University of Pennsylvania.
Sommigen protesteerden luidkeels tegen een wiskundig bewijs zonder wiskundige redenering:
- "Het huidige bewijs steunt in feite op een Orakel, en ik zeg: weg met de Orakels! Dat is geen wiskunde" — Paul Halmos, UC Santa Barbara.
- "Als de oplossing gebruikmaakt van computerverificatie van speciale gevallen... dan behoort zo'n oplossing helemaal niet tot de wiskundige wetenschap" — Frank Bonsall, University of Edinburgh.
- "Het toelaten van de computertrucs van Appel en Haken tot de rangen van de wiskunde zou ons intellectueel onvervuld achterlaten" — Daniel Cohen, Hunter College NYC.
Anderen weigerden zelfs te geloven dat er überhaupt een bewijs was gevonden:
"Niet alleen is er geen bewijs te vinden in wat ze hebben gepubliceerd, maar er is niets dat überhaupt op een bewijs lijkt... Het is het meest belachelijke geval van 'De nieuwe kleren van de keizer' dat ooit de geschiedenis van de wiskunde heeft beschaamd" — George Spencer-Brown, Cambridge University.
Een hoofd van een wiskundige afdeling weigerde Appel en Haken te laten meeten met zijn promovendi, omdat hij beweerde dat hun methode de stimulans wegnam om een verifieerbaar en eleganter bewijs te vinden:
"Aangezien het probleem was opgelost door middel van een totaal ongeschikte methode, zou geen enkele eersteklas wiskundige er nu meer aan werken, omdat hij dan niet de eerste zou zijn die het deed, en daarom zou een fatsoenlijk bewijs onbepaald kunnen worden uitgesteld." (overgeleverd door Robin Wilson in Four Colors Suffice).
Op amusante — en voorspelbare — wijze leek leeftijd de bepalende factor te zijn in de ontvankelijkheid voor computerondersteunde bewijzen. Na een presentatie over het bewijs door de zoon van Haken (die zijn vader had geholpen), splitste het publiek zich naar verluidt in twee groepen: "de 40-plussers konden niet worden overtuigd dat een bewijs door een computer correct was, terwijl de onder-40-jarigen niet konden worden overtuigd dat een bewijs dat uit 700 pagina's handmatige berekeningen bestond, correct kon zijn." (via het boek Four Colors Suffice van Robin Wilson).
Geloofwaardigheid
Het bewijs kreeg enkele prominente steunbetuigingen. De legendarische wiskundige Bill Tutte — die aanvankelijk in een tijdschrift openlijk twijfelde aan de gekozen computerondersteunde methode — zou uiteindelijk toegeven dat het probleem was opgelost en dit vieren met een gedicht:
Wolfgang Haken Sloeg de Kraken Eén! Twee! Drie! Vier! Sprak hij: "Het monster is niet meer."
De gerespecteerde Duitse wiskundige Heinrich Heesch accepteerde het bewijs, zij het met tegenzin, aangezien hij vier decennia aan het probleem had gewerkt en zelfs de belangrijkste algoritmische methoden had gecreëerd die door Appel en Haken werden toegepast. Ook andere wiskundigen namen het bewijs serieus, zoals Ted Swart, die rond dezelfde tijd zelf een computerondersteund bewijs had ontwikkeld, maar net werd ingehaald.
Media-aandacht
Prominente steun hielp het bewijs aan geloofwaardigheid en zorgde voor koppen in de media, met uitzondering van The New York Times. De redacteuren daar weigerden de doorbraak te verslaan uit angst dat het een vals alarm was. Toen het maanden later als legitiem werd beschouwd, voerden de redacteuren aan dat het niet langer nieuwswaardig was. Het verscheen uiteindelijk alleen in de krant dankzij een opiniestuk van Lipman Bers, president van The American Mathematical Society.
Filosofie
Het debat over 'bewijs zonder redenering' intensiveerde in 1979, toen filosoof Thomas Tymoczko in The Journal of Philosophy betoogde dat een bewijs dat niet volledig door een mens kan worden gecontroleerd, geen traditioneel wiskundig bewijs was (hoewel hij niet twijfelde aan het feit dat het bewijs technisch bewees wat het claimde).
"Geen enkele wiskundige heeft een bewijs van de 4CT gezien, noch heeft iemand een bewijs gezien dat er een bewijs voor is. Bovendien is het zeer onwaarschijnlijk dat enige wiskundige ooit een bewijs van de 4CT zal zien." — Thomas Tymoczko.
Ted Swart reageerde op Tymoczko in een antwoord gepubliceerd in American Mathematical Monthly. Hij vatte zijn argument later samen door te zeggen: "Ik beschouw een computerondersteund bewijs simpelweg als een uitbreiding van potlood en papier." Swart trok ook de impliciete onfeilbaarheid van menselijke wiskundigen in twijfel: "Mensen worden moe, hun aandacht dwaalt af en ze zijn al te vatbaar voor diverse soorten fouten... Computers worden niet moe." Zijn weerlegging zou later een prijs winnen voor uiteenzettend schrijven.
En nu?
In het boek van Robin Wilson over de geschiedenis van de stelling werd opgemerkt dat Bill Tutte in 1978 de vraag stelde wat de toekomst hield voor wiskundigen in het licht van door machines gemaakte bewijzen:
"Ik stel me een van hen voor die wanhopig uitroept: 'Wat moet ik nu doen?'"
Zijn advies? "Wees goed gehumeurd. Je kunt verdergaan in dezelfde algemene onderzoekslijn." En natuurlijk bood hij ook een gedicht aan:
De Vierkleurenstelling is het topje van de ijsberg, het dunne uiteinde van de wig en de eerste koekoek van de lente. Dit is, zonder twijfel, geschreven door een mens.
Voor een uitgebreid verslag van deze geschiedenis kan men kijken naar het boek Four Colors Suffice: How the Map Problem Was Solved van Robin Wilson.
De eerste keer dat machines wiskundigen overtroffen
In juli 1976 werd een wiskundig mysterie dat wiskundigen al meer dan een eeuw verbijsterde eindelijk opgelost: de Vierkleurenstelling.
Definitie: Vierkleurenstelling De Vierkleurenstelling stelt dat er niet meer dan vier kleuren nodig zijn om de regio's van elke willekeurige kaart zo in te kleuren dat geen twee aangrenzende regio's dezelfde kleur hebben.
De auteurs — Kenneth Appel en Wolfgang Haken — schreven het succes toe aan een onconventionele collaborator: een computer had een groot deel van het zware wiskundige werk verricht, om precies te zijn 1.200 uur rekentijd en 10 miljard beslissingen. De computerprogrammeur John Koch hielp Appel en Haken bij het algoritmische werk.
Appel en Haken zouden later beschrijven hoe het systeem hen "dingen begon te leren over hoe we verder moesten gaan die we nooit hadden verwacht", waarbij ze toegaven dat het systeem de makers op bepaalde intellectuele taken was "ontstegen". Een nieuwe wereld van mens-machine-wiskunde was begonnen, wat de vraag opriep: kunnen we vertrouwen op een wiskundig bewijs dat te omvangrijk is voor een mens om te verifiëren?
Ontvangst
De reacties van wiskundigen varieerden van acceptatie tot afwijzing en zelfs ontkenning, in plaats van universele bewondering. Wiskundigen, die trots zijn op hun rationaliteit, werden plotseling geconfronteerd met een wiskundige 'moloch' in wat moet hebben gevoeld als religieuze ketterij.
"God zou niet toelaten dat de stelling werd bewezen door een methode die zo verschrikkelijk is!" — Herbert Wilf, University of Pennsylvania.
Sommigen protesteerden luidkeels tegen een wiskundig bewijs zonder wiskundige redenering:
- "Het huidige bewijs steunt in feite op een Orakel, en ik zeg: weg met de Orakels! Dat is geen wiskunde" — Paul Halmos, UC Santa Barbara.
- "Als de oplossing gebruikmaakt van computerverificatie van speciale gevallen... dan behoort zo'n oplossing helemaal niet tot de wiskundige wetenschap" — Frank Bonsall, University of Edinburgh.
- "Het toelaten van de computertrucs van Appel en Haken tot de rangen van de wiskunde zou ons intellectueel onvervuld achterlaten" — Daniel Cohen, Hunter College NYC.
Anderen weigerden zelfs te geloven dat er überhaupt een bewijs was gevonden:
"Niet alleen is er geen bewijs te vinden in wat ze hebben gepubliceerd, maar er is niets dat überhaupt op een bewijs lijkt... Het is het meest belachelijke geval van 'De nieuwe kleren van de keizer' dat ooit de geschiedenis van de wiskunde heeft beschaamd" — George Spencer-Brown, Cambridge University.
Een hoofd van een wiskundige afdeling weigerde Appel en Haken te laten meeten met zijn promovendi, omdat hij beweerde dat hun methode de stimulans wegnam om een verifieerbaar en eleganter bewijs te vinden:
"Aangezien het probleem was opgelost door middel van een totaal ongeschikte methode, zou geen enkele eersteklas wiskundige er nu meer aan werken, omdat hij dan niet de eerste zou zijn die het deed, en daarom zou een fatsoenlijk bewijs onbepaald kunnen worden uitgesteld." (overgeleverd door Robin Wilson in Four Colors Suffice).
Op amusante — en voorspelbare — wijze leek leeftijd de bepalende factor te zijn in de ontvankelijkheid voor computerondersteunde bewijzen. Na een presentatie over het bewijs door de zoon van Haken (die zijn vader had geholpen), splitste het publiek zich naar verluidt in twee groepen: "de 40-plussers konden niet worden overtuigd dat een bewijs door een computer correct was, terwijl de onder-40-jarigen niet konden worden overtuigd dat een bewijs dat uit 700 pagina's handmatige berekeningen bestond, correct kon zijn." (via het boek Four Colors Suffice van Robin Wilson).
Geloofwaardigheid
Het bewijs kreeg enkele prominente steunbetuigingen. De legendarische wiskundige Bill Tutte — die aanvankelijk in een tijdschrift openlijk twijfelde aan de gekozen computerondersteunde methode — zou uiteindelijk toegeven dat het probleem was opgelost en dit vieren met een gedicht:
Wolfgang Haken Sloeg de Kraken Eén! Twee! Drie! Vier! Sprak hij: "Het monster is niet meer."
De gerespecteerde Duitse wiskundige Heinrich Heesch accepteerde het bewijs, zij het met tegenzin, aangezien hij vier decennia aan het probleem had gewerkt en zelfs de belangrijkste algoritmische methoden had gecreëerd die door Appel en Haken werden toegepast. Ook andere wiskundigen namen het bewijs serieus, zoals Ted Swart, die rond dezelfde tijd zelf een computerondersteund bewijs had ontwikkeld, maar net werd ingehaald.
Media-aandacht
Prominente steun hielp het bewijs aan geloofwaardigheid en zorgde voor koppen in de media, met uitzondering van The New York Times. De redacteuren daar weigerden de doorbraak te verslaan uit angst dat het een vals alarm was. Toen het maanden later als legitiem werd beschouwd, voerden de redacteuren aan dat het niet langer nieuwswaardig was. Het verscheen uiteindelijk alleen in de krant dankzij een opiniestuk van Lipman Bers, president van The American Mathematical Society.
Filosofie
Het debat over 'bewijs zonder redenering' intensiveerde in 1979, toen filosoof Thomas Tymoczko in The Journal of Philosophy betoogde dat een bewijs dat niet volledig door een mens kan worden gecontroleerd, geen traditioneel wiskundig bewijs was (hoewel hij niet twijfelde aan het feit dat het bewijs technisch bewees wat het claimde).
"Geen enkele wiskundige heeft een bewijs van de 4CT gezien, noch heeft iemand een bewijs gezien dat er een bewijs voor is. Bovendien is het zeer onwaarschijnlijk dat enige wiskundige ooit een bewijs van de 4CT zal zien." — Thomas Tymoczko.
Ted Swart reageerde op Tymoczko in een antwoord gepubliceerd in American Mathematical Monthly. Hij vatte zijn argument later samen door te zeggen: "Ik beschouw een computerondersteund bewijs simpelweg als een uitbreiding van potlood en papier." Swart trok ook de impliciete onfeilbaarheid van menselijke wiskundigen in twijfel: "Mensen worden moe, hun aandacht dwaalt af en ze zijn al te vatbaar voor diverse soorten fouten... Computers worden niet moe." Zijn weerlegging zou later een prijs winnen voor uiteenzettend schrijven.
En nu?
In het boek van Robin Wilson over de geschiedenis van de stelling werd opgemerkt dat Bill Tutte in 1978 de vraag stelde wat de toekomst hield voor wiskundigen in het licht van door machines gemaakte bewijzen:
"Ik stel me een van hen voor die wanhopig uitroept: 'Wat moet ik nu doen?'"
Zijn advies? "Wees goed gehumeurd. Je kunt verdergaan in dezelfde algemene onderzoekslijn." En natuurlijk bood hij ook een gedicht aan:
De Vierkleurenstelling is het topje van de ijsberg, het dunne uiteinde van de wig en de eerste koekoek van de lente. Dit is, zonder twijfel, geschreven door een mens.
Voor een uitgebreid verslag van deze geschiedenis kan men kijken naar het boek Four Colors Suffice: How the Map Problem Was Solved van Robin Wilson.
Groetjes,