In dit artikel reflecteert Mike McCoy op een recent preprint van Wang & Wu, waarin de Sferische Hadwiger-conjectuur blijkbaar is bewezen met hulp van OpenAI Codex. De auteur merkt op dat AI in staat is om complexe bewijstappen uit te werken en hiaten te dichten, taken die voorheen uitsluitend door onderzoekswiskundigen op hoog niveau werden uitgevoerd.
McCoy trekt een parallel met klassieke muziek: net zoals muziek naar het conservatorium is verplaatst om als cultureel reliek bewaard te blijven, zou wiskunde een soortgelijk lot kunnen krijgen. Hij stelt dat de traditionele prikkelstructuren en financiering in de academische wereld niet langer passen bij een realiteit waarin AI superieure intellectuele prestaties levert. Hij pleit voor een nieuwe manier om menselijke wiskundigen te ondersteunen, niet vanwege hun productiviteit, maar vanwege de culturele en existentiële waarde van het menselijk streven om de realiteit te begrijpen.
Staat de wiskunde op het punt om naar het conservatorium te gaan?
In dezelfde week dat Claude het bewijs van de Laatste Stelling van Fermat formaliseerde in Lean, landde er een artikel in mijn inbox getiteld The Spherical Hadwiger Theorem. De Sferische Hadwiger-conjectuur[^1], die sinds ongeveer 1974 openstaat, beschrijft een niche maar belangrijk onderdeel van de integraal-geometrische mechanismen. Ik zal hier niet ingaan op de details van de conjectuur; wie geïnteresseerd is, kan een discussie vinden in mijn vorige bericht, waarin het theorema (toen nog een conjectuur[^2]) het bewijs van een klein lemma uit mijn promotietijd aanzienlijk vereenvoudigt.
Maar om bij het punt te komen: dit nieuwe preprint van Wang & Wu van de Hunan University bewijst de conjectuur blijkbaar met behulp van AI. De laatste sectie bevat de volgende disclaimer:
Tijdens de voorbereiding van dit manuscript is OpenAI Codex gebruikt om te helpen bij het uitwerken van details van het bewijs, het identificeren van hiaten en punten die verduidelijking behoeven, het organiseren en opmaken van het manuscript, en het redigeren van het Engels. De auteurs hebben alle door AI ondersteunde wiskundige inhoud beoordeeld en geverifieerd, voorgestelde wijzigingen doorgevoerd, alle definitieve wiskundige en redactionele beslissingen genomen en dragen de volledige verantwoordelijkheid voor het manuscript.
Deze disclaimer laat de mogelijkheid open dat Codex een aanzienlijk deel van het werk heeft verricht dat tot zeer kort geleden een wiskundige op onderzoeksniveau vereiste: het uitwerken van bewijsdetails[^3], het vinden en dichten van hiaten, en blijkbaar het schrijven van het artikel. Bovendien is het werk zeer gepolijst en leesbaar (voor wie een onderzoekswiskundige in dit vakgebied is).
Om duidelijk te zijn: ik heb het bewijs nog niet volledig geverifieerd. Ik heb het samen met Claude Fable doorgenomen en het overleeft de eerste inspectie, maar het volledig doorgronden zal meer energie kosten dan ik op dit moment heb. Dit is geen kritiek op Wang & Wu—dit lijkt een uitstekend artikel te zijn dat de moeite waard is om te bestuderen. Ze hebben zelfs alle principes voor AI-gebruik gevolgd zoals uiteengezet in de Leidense Verklaring.
Een mijlpaal, dicht bij huis
Voor mij komt het bewijs van het Sferische Hadwiger-theorema dicht bij huis. Ik heb tijdens mijn promotie geprobeerd het te bewijzen, en eerder dit jaar heb ik met behulp van AI nog een halfslachtige poging gewaagd. Het is geen theorema dat de koppen haalt, maar dat heeft het niet gered.
Ik had niet verrast mogen zijn. Toen GPT-4 werd gelanceerd, publiceerde OpenAI een rapport over de potentiële impact van LLM's op de arbeidsmarkt. De blootstelling van het werk van wiskundigen aan verstoringen door AI was de hoogste van alle gemodelleerde categorieën; het whitepaper schatte dat 100% van het werk van een wiskundige blootgesteld was aan LLM's, over drie verschillende arbeidsmodellen heen. Dat was hoger dan bij schrijvers, vertalers, kunstenaars en grafisch ontwerpers. Het enige verschil is dat het voor wiskundigen iets langer duurde voordat ze de pijn begonnen te voelen.
Het is verleidelijk, zij het enigszins arrogant, om te beweren dat deze vertraging in de dominantie van LLM's in de wiskunde voortkwam uit het feit dat wiskunde op onderzoeksniveau tot de meest uitdagende menselijke ondernemingen behoort. Ik vermoed dat de vertraging evenzeer te wijten is aan het feit dat onderzoekswiskunde minder economische waarde—en minder trainingsdata—heeft dan deze andere creatieve domeinen.
Naar het conservatorium?
Denk aan klassieke muziek. Onze samenleving ondersteunt klassieke musici niet op dezelfde manier als we 'populaire' musici ondersteunen. Klassieke muziek is geïnstitutionaliseerd, naar het conservatorium gestuurd als een reliek. Een klein segment van de samenleving heeft besloten dat het vermogen om deze muziek uit te voeren het waard is om bewaard te blijven, en wijdt een fractie van het kapitaal aan dat doel: het opleiden van jongeren en het betalen van een paar van de beste spelers in de grootste steden om dit professioneel te doen.
Zou dit model kunnen werken voor wiskundigen? Het is makkelijk voor te stellen: in de tijd van Euclides bestond wiskunde grotendeels als een intellectuele bezigheid die waardig was voor een paar begaafde mensen. Een wiskundig conservatorium zou de wiskunde kunnen helpen bloeien, zelfs wanneer het niet langer moeilijk is om nieuwe resultaten te creëren, maar enkel moeilijk om hun belang te begrijpen en te communiceren.
Maar zuivere wiskunde bevindt zich al in een conservatorium, beter bekend als de academie. Buiten de universiteit blijven de banen voor zuivere wiskundigen schaars. De resultaten worden slechts begrepen door een selecte groep. Maakt het überhaupt uit dat de moeilijke resultaten binnenkort allemaal door computers zullen worden bewezen?
De kern van de zaak
Het is het waard om mensen te blijven ondersteunen in de culturele onderneming die we momenteel "onderzoekswiskunde" noemen. Wiskunde, en in het bijzonder zuivere wiskunde, is altijd gegaan over het vertellen van verhalen die ons helpen de realiteit dieper te begrijpen. Door te vereenvoudigen en te abstraheren, beginnen we de verborgen structuur te zien: parallelle lijnen kruisen elkaar nooit, de sfeer ziet er in elke richting hetzelfde uit, de priemgetallen houden nooit op. Maar de huidige ondersteuningssystemen voor wiskundigen, net als in zoveel andere menselijke creatieve velden, moeten drastisch veranderen om om te kunnen gaan met de nieuwe realiteit van AI.
De prikkelstructuren die dit werk ondersteunen zijn ongeschikt voor wat AI brengt. Deze tools maken het moeilijker om te bepalen of een complex argument überhaupt correct is, laat staan wie financiering, vaste aanstellingen en roem verdient. De keuze waar we voor staan is: hoe zorgen we ervoor dat mensen relevant blijven wanneer hun intellectuele inspanningen simpelweg niet op kunnen boksen tegen computers? Wanneer intelligentie alleen nog wordt beperkt door silicium en elektriciteit, zullen we dan bereid zijn een cultuur te blijven ondersteunen waarin wiskundigen bestaan? Ik hoop het zeer.
***
[^1]: Zie Probleem 3 in de thesis van Glasauer. [^2]: Sterker nog, het was pas nadat ik het initiële blogbericht schreef dat prof. Rolf Schneider me herinnerde aan het feit dat de conjectuur op dat moment nog openstond. [^3]: Welke bewijsdetails precies? Ik zou graag het volledige chattranscript zien. Hoewel het bewijs de ruwe aanpak van Klain en Rota voor het Euclidische theorema volgt, vereisen de details het overwinnen van verschillende grote obstructies, en ik ben benieuwd hoeveel daarvan werden geïdentificeerd en opgelost door GPT 5.6.
Staat de wiskunde op het punt om naar het conservatorium te gaan?
In dezelfde week dat Claude het bewijs van de Laatste Stelling van Fermat formaliseerde in Lean, landde er een artikel in mijn inbox getiteld The Spherical Hadwiger Theorem. De Sferische Hadwiger-conjectuur[^1], die sinds ongeveer 1974 openstaat, beschrijft een niche maar belangrijk onderdeel van de integraal-geometrische mechanismen. Ik zal hier niet ingaan op de details van de conjectuur; wie geïnteresseerd is, kan een discussie vinden in mijn vorige bericht, waarin het theorema (toen nog een conjectuur[^2]) het bewijs van een klein lemma uit mijn promotietijd aanzienlijk vereenvoudigt.
Maar om bij het punt te komen: dit nieuwe preprint van Wang & Wu van de Hunan University bewijst de conjectuur blijkbaar met behulp van AI. De laatste sectie bevat de volgende disclaimer:
Tijdens de voorbereiding van dit manuscript is OpenAI Codex gebruikt om te helpen bij het uitwerken van details van het bewijs, het identificeren van hiaten en punten die verduidelijking behoeven, het organiseren en opmaken van het manuscript, en het redigeren van het Engels. De auteurs hebben alle door AI ondersteunde wiskundige inhoud beoordeeld en geverifieerd, voorgestelde wijzigingen doorgevoerd, alle definitieve wiskundige en redactionele beslissingen genomen en dragen de volledige verantwoordelijkheid voor het manuscript.
Deze disclaimer laat de mogelijkheid open dat Codex een aanzienlijk deel van het werk heeft verricht dat tot zeer kort geleden een wiskundige op onderzoeksniveau vereiste: het uitwerken van bewijsdetails[^3], het vinden en dichten van hiaten, en blijkbaar het schrijven van het artikel. Bovendien is het werk zeer gepolijst en leesbaar (voor wie een onderzoekswiskundige in dit vakgebied is).
Om duidelijk te zijn: ik heb het bewijs nog niet volledig geverifieerd. Ik heb het samen met Claude Fable doorgenomen en het overleeft de eerste inspectie, maar het volledig doorgronden zal meer energie kosten dan ik op dit moment heb. Dit is geen kritiek op Wang & Wu—dit lijkt een uitstekend artikel te zijn dat de moeite waard is om te bestuderen. Ze hebben zelfs alle principes voor AI-gebruik gevolgd zoals uiteengezet in de Leidense Verklaring.
Een mijlpaal, dicht bij huis
Voor mij komt het bewijs van het Sferische Hadwiger-theorema dicht bij huis. Ik heb tijdens mijn promotie geprobeerd het te bewijzen, en eerder dit jaar heb ik met behulp van AI nog een halfslachtige poging gewaagd. Het is geen theorema dat de koppen haalt, maar dat heeft het niet gered.
Ik had niet verrast mogen zijn. Toen GPT-4 werd gelanceerd, publiceerde OpenAI een rapport over de potentiële impact van LLM's op de arbeidsmarkt. De blootstelling van het werk van wiskundigen aan verstoringen door AI was de hoogste van alle gemodelleerde categorieën; het whitepaper schatte dat 100% van het werk van een wiskundige blootgesteld was aan LLM's, over drie verschillende arbeidsmodellen heen. Dat was hoger dan bij schrijvers, vertalers, kunstenaars en grafisch ontwerpers. Het enige verschil is dat het voor wiskundigen iets langer duurde voordat ze de pijn begonnen te voelen.
Het is verleidelijk, zij het enigszins arrogant, om te beweren dat deze vertraging in de dominantie van LLM's in de wiskunde voortkwam uit het feit dat wiskunde op onderzoeksniveau tot de meest uitdagende menselijke ondernemingen behoort. Ik vermoed dat de vertraging evenzeer te wijten is aan het feit dat onderzoekswiskunde minder economische waarde—en minder trainingsdata—heeft dan deze andere creatieve domeinen.
Naar het conservatorium?
Denk aan klassieke muziek. Onze samenleving ondersteunt klassieke musici niet op dezelfde manier als we 'populaire' musici ondersteunen. Klassieke muziek is geïnstitutionaliseerd, naar het conservatorium gestuurd als een reliek. Een klein segment van de samenleving heeft besloten dat het vermogen om deze muziek uit te voeren het waard is om bewaard te blijven, en wijdt een fractie van het kapitaal aan dat doel: het opleiden van jongeren en het betalen van een paar van de beste spelers in de grootste steden om dit professioneel te doen.
Zou dit model kunnen werken voor wiskundigen? Het is makkelijk voor te stellen: in de tijd van Euclides bestond wiskunde grotendeels als een intellectuele bezigheid die waardig was voor een paar begaafde mensen. Een wiskundig conservatorium zou de wiskunde kunnen helpen bloeien, zelfs wanneer het niet langer moeilijk is om nieuwe resultaten te creëren, maar enkel moeilijk om hun belang te begrijpen en te communiceren.
Maar zuivere wiskunde bevindt zich al in een conservatorium, beter bekend als de academie. Buiten de universiteit blijven de banen voor zuivere wiskundigen schaars. De resultaten worden slechts begrepen door een selecte groep. Maakt het überhaupt uit dat de moeilijke resultaten binnenkort allemaal door computers zullen worden bewezen?
De kern van de zaak
Het is het waard om mensen te blijven ondersteunen in de culturele onderneming die we momenteel "onderzoekswiskunde" noemen. Wiskunde, en in het bijzonder zuivere wiskunde, is altijd gegaan over het vertellen van verhalen die ons helpen de realiteit dieper te begrijpen. Door te vereenvoudigen en te abstraheren, beginnen we de verborgen structuur te zien: parallelle lijnen kruisen elkaar nooit, de sfeer ziet er in elke richting hetzelfde uit, de priemgetallen houden nooit op. Maar de huidige ondersteuningssystemen voor wiskundigen, net als in zoveel andere menselijke creatieve velden, moeten drastisch veranderen om om te kunnen gaan met de nieuwe realiteit van AI.
De prikkelstructuren die dit werk ondersteunen zijn ongeschikt voor wat AI brengt. Deze tools maken het moeilijker om te bepalen of een complex argument überhaupt correct is, laat staan wie financiering, vaste aanstellingen en roem verdient. De keuze waar we voor staan is: hoe zorgen we ervoor dat mensen relevant blijven wanneer hun intellectuele inspanningen simpelweg niet op kunnen boksen tegen computers? Wanneer intelligentie alleen nog wordt beperkt door silicium en elektriciteit, zullen we dan bereid zijn een cultuur te blijven ondersteunen waarin wiskundigen bestaan? Ik hoop het zeer.
***
[^1]: Zie Probleem 3 in de thesis van Glasauer. [^2]: Sterker nog, het was pas nadat ik het initiële blogbericht schreef dat prof. Rolf Schneider me herinnerde aan het feit dat de conjectuur op dat moment nog openstond. [^3]: Welke bewijsdetails precies? Ik zou graag het volledige chattranscript zien. Hoewel het bewijs de ruwe aanpak van Klain en Rota voor het Euclidische theorema volgt, vereisen de details het overwinnen van verschillende grote obstructies, en ik ben benieuwd hoeveel daarvan werden geïdentificeerd en opgelost door GPT 5.6.
Groetjes,