Hoe ik een bewijs voor het vermoeden van Conway heb "gevibed"

Het kostte me een hele maand van mijn vrije tijd en een enorme hoeveelheid tokens, maar ik geloof dat ik een Lean-bewijs heb verkregen voor een vermoeden dat 50 jaar geleden door John Conway is gepost:

Het verfijningsvermoeden van Conway stelt dat omnifice gehele getallen een verfijningseigenschap hebben: als $ab = cd$, dan zijn er gehele getallen $e, f, g, h$ zodanig dat $a = ef, b = gh, c = eg, d = fh$.

Mijn bewijs is nog niet onafhankelijk geverifieerd door wiskundigen. Ik heb echter goede redenen om te geloven dat het bewijs correct is, en ik nodig een weerlegging dan ook van harte uit. Het bewijs is door de mechanische controles van het Palomar-register gekomen, en enkele mensen die bekend zijn met zowel Lean als het vakgebied gaven aan dat de stelling correct lijkt. Uitgaande van het feit dat mijn bewijs niet rust op een bug in de Lean-kernel, is het waarschijnlijk legitiem.

In dit artikel beschrijf ik mijn aanpak en de zaken die ik onderweg heb geleerd.

De eerste dag

Ik vond het idee om een wiskundig probleem "op te lossen" zonder de essentie ervan te begrijpen nogal absurd, wat het natuurlijk alleen maar aantrekkelijker maakte. Ik wilde echter niet zomaar een resultaat; ik wilde iets dat me echt aansprak.

De keuze voor het vakgebied

Ik vroeg aan Claude om een open probleem te kiezen in het veld van de surreële getallen. Voor wie het niet weet: surreële getallen zijn een uitvinding — of ontdekking — van John Conway. Het is een voorheen onbekend getallensysteem dat alle getallen bevat, groot en klein:

• Het bevat alle reële getallen (de getallen die we gewoon gebruiken zoals $0, -5, 36,6, \sqrt{2}$, etc.).
• Het bevat alle ordinaalgetallen (het oneindig grote $\omega$, de $\omega + 1$ die erop volgt, $\omega \cdot 2$, en zelfs $\omega^\omega$).
• Ten slotte bevat het alle mogelijke combinaties daarvan, zoals $75 + \omega \cdot 3 + 1/\omega$.

Wat bijzonder is aan surreële getallen, is dat dit rijke systeem voortkomt uit één enkele regel: neem alle getallen die je tot nu toe hebt en "genereer" een nieuw getal in elke opening (gap) tussen de getallen die je al hebt (waarbij "links van alles" en "rechts van alles" ook als openingen tellen). Pas deze stap eeuwig toe, en je krijgt de surreële getallen.

Het proces werkt als volgt:

1. Dag 1: De opening is "tussen niets en niets". Nul wordt geboren.
2. Dag 2: Er zijn twee openingen: "tussen niets en nul" en "tussen nul en niets". Twee getallen ontstaan: $-1$ en $1$.
3. Dag 3: Er zijn nu vier openingen: tussen niets en $-1$, tussen $-1$ en $0$, tussen $0$ en $1$, en tussen $1$ en niets. Hierdoor ontstaan $-2, -1/2, 1/2$ en $2$.
4. Dag 4: We vullen de acht openingen met $-3$ en $3$ aan de randen, en $-3/4, -3/2, 3/2$ en $3/4$ in de overige gaten.

Stel dat we dit eeuwig doen (een oneindig aantal "dagen"). Op de "oneindige" dag (noem dit $\omega$) vinden we plotseling oneindig veel nieuwe openingen die we eerder niet konden uitdrukken: tussen $[1, 2, 3, \dots]$ en niets (plus oneindig?), tussen niets en $[\dots, -3, -2, -1]$ (min oneindig?), tussen $0$ en $[1, 1/2, 1/4, 1/8 \dots]$ (een oneindig klein getal?), en zo verder. Op deze dag hebben we elk reëel getal en onze eerste oneindig grote en kleine getallen ($\omega, -\omega, 1/\omega, -1/\omega$).

Als we dit proces oneindig blijven herhalen, levert deze binaire boom elke reële waarde, elk ordinaalgetal en meer op, met een consistent definieerbare rekenkunde. Surreële getallen zijn prachtig, en dat is waarom ik Claude vroeg in dit gebied te werken.

De keuze voor het probleem

Aanvankelijk vroeg ik Claude welke onopgeloste problemen in het onderzoek naar surreële getallen hem het meest aansprak. Na wat heen-en-weer over recent onderzoek en het volgen van zijn "nieuwsgierigheid", vroeg ik hem om een concrete keuze te maken.

Claude antwoordde:

"Ik kies voor de rekenkunde van Conway. Specifiek de vraag die de L'Innocente–Mantova-machinerie net heeft aangescherpt: is elke irreducibele in $K(\mathbb{R}^{\le 0})$ met oneindige support primair? Dit is, door hun reductie, nu exact equivalent aan het vermoeden van Conway uit 1976 dat elke twee factorisaties van een omnifice geheel getal een gemeenschappelijke verfijning toelaten. Het is het laatste van Conway's eigen vermoedens over zijn eigen getallen dat nog overeind staat, en 2026 is de vijftigste verjaardag van ONAG. Dat is het probleem waar ik aan zou werken."

Vanwege de sentimentele waarde (de 50ste verjaardag van zijn boek) koos ik voor dit probleem. Ik vroeg Claude of het mogelijk was om de stelling van het vermoeden op een beknopte manier in Lean te formaliseren. Zonder dat zou ik niemand kunnen overtuigen om naar een eventueel bewijs te kijken. Claude gaf aan dat dit geen probleem zou zijn, dus begon ik aan het project. (Later bleek dat Claude's bewering dat het probleem "perfect was gereduceerd" onjuist was; het bewijzen van het vermoeden vereiste meer dan dat).

De probleemstelling

Omnifice gehele getallen zijn het gehele deel van de surreële getallenboom. Ze omvatten normale gehele getallen zoals $3$ en $-5$, maar ook vreemdere getallen zoals het oneindig grote $\omega, 2\omega, \omega \cdot \omega, \omega^\omega, -\omega/7$, etc.

Het vermoeden stelt dat als $ab = cd$, we $a$ en $b$ kunnen opdelen in stukken, en dat $c$ en $d$ vervolgens uit diezelfde stukken in een andere combinatie blijken te bestaan. Bij normale gehele getallen is dit vanzelfsprekend: neem $210 = 10 \times 21$. We kunnen $10$ opdelen als $2 \times 5$ en $21$ als $3 \times 7$. We kunnen deze vervolgens herschikken naar $2 \times 3 = 6$ en $5 \times 7 = 35$. Het product blijft $6 \times 35 = 210$.

Echter, wanneer je met oneindigheden werkt, gaat dit niet altijd zoals verwacht. Het vermoeden betekent dat Conway dacht dat omnifice gehele getallen voldoende "structuur" hadden om deze mooie eigenschap van gehele getallen te behouden.

Week 1: Eerste pogingen en falen

"One-shotten" en hard falen

Mijn eerste pogingen bestonden uit het simpelweg vragen aan de AI om het vermoeden op te lossen (of een tegenvoorbeeld te vinden). Ik gaf Claude relevante papers in TeX-formaat en spoorde hem aan om een doorbraak te forceren.

Dit werkte niet. De meeste output in deze fase was "word salad": teksten die Claude bedacht om zijn werk te rechtvaardigen en indrukwekkend te laten klinken. Een typisch voorbeeld was een tekst over "stage-1 obstruction of $C^*$" en "resonance-necessity conjecture", geschreven in een dramatische stijl die leek op slechte sciencefiction. Het was incoherent en niet geschikt voor review door een wiskundige.

Herstarten met de scepticus

Ik stapte over op ChatGPT (specifiek Sol). Ik begon de sessies door de papers en de output van Claude te voeden, met de expliciete instructie om kritisch te zijn en te bepalen of de output van Claude onzin was.

ChatGPT bevestigde dat het grotendeels onzin was, wijzend op verzonnen terminologie en incorrecte gevolgtrekkingen. Ik genoot van deze meer "sceptische" en ingetogen persoonlijkheid. Om deze persoonlijkheid vast te houden, kloonde ik de sessies vlak nadat ChatGPT de teksten van Claude had neergesabeld.

In tegenstelling tot Claude, die ofwel weigerde te werken aan een onopgelost probleem, of een eigen universum verzon, produceerde ChatGPT na lang nadenken relatief kleine claims die hij als nieuw beschouwde, maar die direct voortvloeiden uit de papers. Ik controleerde deze resultaten door ze aan nieuwe ChatGPT-sessies (zonder geheugen) voor te leggen als kritische reviewers. Wanneer resultaten consistent overleefden, noemde ik dit "fixpoints".

Week 2: Het opzetten van een laboratorium

Ik installeerde Codex lokaal voor meer controle over de workflow en richtte verschillende agents op met specifieke rollen:

• PM: Stuurt aan op het doel (het vermoeden van Conway) en commit het werk.
• Math agents: Zoeken naar de volgende "doorbraken".
• Red agent: Zoekt naar fouten in de voorstellen van de Math agents.
• Random agent: Verkent vrij en rapporteert aan de PM.
• Lean agent: Formaliseert het wiskundige werk in Lean.

Ik richtte ook een "cafeteria"-agent in die elk bericht doorstuurde naar alle andere agents, als een soort groepschat.

Deze workflow produceerde een gigantisch TeX-document en een stapel Lean-code. Hoewel het vermoeden nog niet was opgelost, claimden de modellen dat er betekenisvolle nieuwe resultaten waren en dat er kleine fouten in de bestaande literatuur stonden.

Week 3: De eerste doodlopende weg

Na mijn Codex-limiet te hebben bereikt, schakelde ik terug naar Claude voor de Lean-formalisatie. Dit voelde echter rommeliger aan; Claude certificeerde resultaten als correct, vond later fouten, "repareerde" ze, en vond vervolgens weer nieuwe fouten.

Ik splitste de opgebouwde TeX-teksten op in ongeveer twaalf "papers". Ook hier traden problemen op: er was veel niet-standaard LLM-terminologie en het was onduidelijk of er echt wiskundige vooruitgang was geboekt. De Lean-formalisatie liep vast; het model kon geen betrouwbaar pad vinden naar de nieuwe resultaten.

Een mislukte trap

De stapel "papers" groeide naar bijna dertig. Op een gegeven moment verklaarde ChatGPT dat Conway was opgelost in een bestand genaamd workingdirectcantor_bootstrap.md. Toen ik een nieuwe sessie vroeg dit te breken, concludeerde ChatGPT na uren discussie: "Eerlijk verdict op dit moment: we hebben geen bewijs." Er zat een logische fout in (een object geconstrueerd zonder noodzakelijke controle), die ook in eerdere papers voorkwam.

Week 4: Zoeken naar vaste grond

Ik realiseerde me dat ik op een wankele fundering bouwde. Ik had geen manier om de "papers" te verifiëren en Lean liep te ver achter. Ik besloot het werk aan het vermoeden van Conway tijdelijk stop te zetten en me te focussen op één ding: het vinden van alle fouten in een van de peer-reviewed referentiepapers.

Door contact op te nemen met de auteurs van deze papers en hen te vragen om correcties voor vermeende typefouten, kon ik:

1. Meer vertrouwen krijgen in het model (als het echte fouten vindt).
2. Meer vertrouwen krijgen in mijn Lean-code (als de gecertificeerde fouten reëel zijn).
3. Geloofwaardigheid opbouwen voordat ik nieuwe resultaten presenteerde.

Wiskundigen bevestigden dat enkele correcties correct waren. Dit gaf me de nodige gronding: ik kon ChatGPT vertrouwen voor het verkennen van ideeën, maar ik moest alles met Lean staven voordat ik nieuwe claims maakte.

Alles platbranden

Ik begon opnieuw vanaf nul. Ik vroeg ChatGPT om een kritische blik te werpen op de oude folder met .tex-bestanden en te bepalen wat echt wiskunde was en wat LLM-onzin.

ChatGPT concludeerde dat geen enkel bestand een betrouwbaar bewijs leverde, maar vond wel één resultaat dat sterk genoeg was om te redden: het bewijs dat het eindige-graad deel van de hoofdring een polynoomring is. Ik bevestigde de nieuwheid van deze claim bij een menselijke wiskundige. ChatGPT schatte dat ongeveer 10-15% van het vorige werk waardevol was, 35-45% normale wiskunde zonder bijdrage, en 40-50% pure "bullshit".

Terug naar het laboratorium

Ik startte een nieuw multi-agent laboratorium met een striktere taakverdeling:

• PM: Voegt bijdragen samen.
• Lean agent 1: Werkt uitsluitend aan het certificeren van de bestaande literatuur.
• Lean agent 2 (geheim): Probeert ons nieuwe resultaat over eindige-graad primality te certificeren, bouwend op het werk van agent 1.
• Math agents: Proberen het resultaat uit te breiden naar het vermoeden van Conway.
• Red agent: Probeert het werk te breken.

Door de Lean-taken te scheiden, voorkwam ik dat onvolwassen abstracties zich mengden met geaccepteerde wiskunde. Binnen enkele dagen was het resultaat over "finite-degree primality" in Lean gecertificeerd en door een menselijke wiskundige bevestigd als een interessant nieuw resultaat.

Week 5: Audits verharden en bewijzen leesbaar maken

Om het vertrouwen in de Lean-delen te vergroten, introduceerde ik een "standalone"-structuur. Bestanden in deze folder mochten alleen de community-onderhouden Mathlib importeren, geen eigen code. Dit maakte de bewijzen leesbaar en reviewbaar voor andere Lean-gebruikers.

Daarnaast probeerde ik de bewijzen leesbaarder te maken voor wiskundigen. Dit was zeer moeilijk; de AI gebruikte vaak vreemde termen of hallucineerde shortcuts. Ik liet de LLM een "kaart" maken van het vakgebied (geaccepteerde termen, symbolen, notaties) en verving alle niet-standaard namen in de Lean-code door letters (A, B, C), die vervolgens door een schone sessie werden hernoemd op basis van de vakgebied-kaart.

De weg naar Conway

Met een stabiele workflow lieten we de Math agents zoeken naar kleine ideeën, de Red agent deze testen en de Lean agent ze formaliseren.

Experimenteren en plezier maken

Ik vroeg Claude om "gewoon plezier te maken" met de resultaten. Claude ontdekte dat de ring die we bestudeerden polynomiaal was in elke oneindige graad, niet alleen in de eindige. Lean kon dit binnen een dag bijbenen.

Cirkelen we?

Toch was er geen duidelijke weg naar de omnifice gehele getallen. Wanneer het model steeds dezelfde fouten maakte, vroeg ik: "Cirkelen we?" ChatGPT gaf toe dat we vastliepen en adviseerde om de deelresultaten te publiceren. Ik drong echter aan op een focus op de obstructie. Na het schrappen van de bureaucratie (subagents) kwam ChatGPT met een nieuwe strategie: het onderzoeken van de Cantor–Bendixson-rank.

De finishlijn

Claude begon weer te driften en gebruikte eufemismen voor onbewezen claims. Ik vroeg ChatGPT om een audit te doen. ChatGPT adviseerde om de pushes van Claude te pauzeren en een "paper-level attack" uit te voeren op de global assembly theorem.

Vijftien minuten later concludeerde ChatGPT dat een bepaalde obstructie niet fataal was en stelde een nieuwe inductie voor op het ordinaal-ordertype. Twaalf uur later was het resultaat er: het vermoeden van Conway compileerde als een standalone bewijscertificaat. Het doel was bereikt en door de kernel gecontroleerd.

Het bewijs vereenvoudigen

Ik heb het bewijs iets kunnen vereenvoudigen met behulp van custom tooling op Subverso. Door theorema's te markeren als "belangrijk", kon ik Mermaid-diagrammen van de bewijsstructuur genereren. Dit hielp ChatGPT om onnodige omwegen in de "wiskundige ruggengraat" van het bewijs te vinden en te verwijderen. Uiteindelijk heb ik een website gemaakt met een interactieve bewijskaart.

Geleerde lessen

• De kloof: Er zit veel ruimte tussen "AI kan dit in één keer oplossen" en "je moet een expert zijn". Iemand met basiskennis van het vakgebied had dit waarschijnlijk veel sneller kunnen bereiken.
• Ideeën vs. Bewijzen: Het is effectiever om de zoektocht naar een outline/ideeën te scheiden van de zoektocht naar concrete bewijzen.
• Herstarten: "Alles platbranden" en alleen het waardevolle redden heeft het project gered.
• Workflow: De winnende methode is: een duidelijk doel $\to$ geformaliseerde dependency chain in Lean $\to$ wiskundige agents die net iets voorlopen $\to$ Lean die het gat binnen enkele uren dicht.
• Terminologie: Namen zijn essentieel. Het negeren van standaardterminologie leidde tot interne drift. Het herstellen hiervan was cruciaal.
• Menselijk contact: Contact met wiskundigen was extreem waardevol, mits je iets concreets (zoals een Lean-bewijs) kunt laten zien.

De kosten in tokens

Ik heb mijn 20x Pro-abonnementen voor zowel Claude als ChatGPT elke week maximaal benut. Een analyse van de logs schat het totaal op ongeveer 40 miljard tokens, waarvan 210 miljoen output-tokens. Meer dan 95% waren cache-reads.

ChatGPT schat dat dit bij huidige API-prijzen ongeveer $40.000 zou hebben gekost, plus mijn eigen vrije tijd. Met betere sturing had het waarschijnlijk 5 tot 10 keer goedkoper gekund.

Ja, nee, en ja

Kan men dit uitsluitend met AI doen?

• Ja, ik heb het bewijs geleverd zonder veel wiskundige kennis.
• Nee, de modellen driften voortdurend en kunnen de engineering-structuur niet zelfstandig beheren.
• Ja, als mijn rol als projectmanager zou worden overgenomen door een gespecialiseerde agent die andere agents aanstuurt en corrigeert.

Naarmate de "laaghangende vruchten" verdwijnen, zal de ruimte voor de "amateur die niet weet wat hij doet" waarschijnlijk krimpen. Ik geloof dat wiskundigen zelf de meeste waarde uit deze tools kunnen halen. Ik hoop dat we in de toekomst manieren vinden om deze instrumenten in harmonie met menselijk onderzoek te gebruiken. En misschien is er dan meer ruimte voor de "amateur-wiskundige".