Wiskundigen wegen AI-bewijs van GPT-5.6 Sol Ultra

Half juli zette OpenAI een pdf online met een opmerkelijke claim: het model GPT-5.6 Sol Ultra zou een wiskundig vermoeden hebben bewezen waar onderzoekers al een halve eeuw op stuklopen. Ruim twee weken later is de vraag verschoven van “kan een AI dit?” naar “klopt het bewijs?”. Die controle ligt voorlopig volledig bij mensen. AI Feiten beschreef eerder de oorspronkelijke claim; nu is het tijd voor de weging.

Een bewijs in minder dan een uur

Het gaat om het cyclus-dubbeldekkingsvermoeden, in de jaren zeventig los van elkaar geformuleerd door George Szekeres en Paul Seymour. Het stelt dat je in elke brugloze graaf een verzameling cykels kunt kiezen waarbij elke rand in precies twee van die cykels zit. GPT-5.6 Sol Ultra kreeg de opdracht minstens acht uur te rekenen, maar leverde binnen een uur een uitwerking, meldt The Decoder. Het model verdeelde het werk over 64 parallelle subagenten, waarvan een deel bewust in het ongewisse werd gelaten over welke aanpak kansrijk leek, zodat ze onafhankelijk bleven zoeken. Andere agenten speelden advocaat van de duivel en testten kandidaat-bewijzen op klassieke fouten. Volgens Developers Digest kostte een reguliere run zo’n 275 tot 485 dollar aan rekentijd.

Mooi, maar zonder bronvermelding

De eerste inhoudelijke reactie kwam van Thomas Bloom, wiskundige aan de Universiteit van Manchester. Hij noemt het “een heel mooi bewijs” en tekent er meteen bij aan dat het kort en elementair is: het had in de jaren tachtig al gevonden kunnen worden. De uitwerking bouwt voort op een artikel uit 1983 van Bermond, Jackson en Jaeger en leunt op technieken die al dertig jaar in de gereedschapskist van grafentheoretici liggen. Bloom heeft ook kritiek. Het bewijs verwijst nergens naar dat eerdere werk, terwijl de invloed ervan zichtbaar is. Zo blijft de vraag hangen of het model echt iets nieuws bedacht of vooral bestaande stukken slim opnieuw combineerde zonder de herkomst te noemen.

Geen Lean, dus nog mensenwerk

Op sociale media namen veel mensen aan dat OpenAI het bewijs had laten controleren met een proof assistant zoals Lean. Dat is niet gebeurd. Volgens de discussie op Hacker News, samengevat door Developers Digest, is er nog geen bewijssysteem volwassen genoeg voor gevorderde grafentheorie. De verificatie leunt daardoor op wiskundigen die de redenering regel voor regel nalopen, zoals eerder gebeurde bij het formaliseren van Fermats laatste stelling. AI Weekly vat de status nuchter samen: een pdf op de server van een bedrijf is geen peer review. Grafentheoretici gaan er de komende weken doorheen voordat iemand het bewijs echt kan afvinken.

Wat betekent dit

Dit verhaal is interessanter dan de eerste koppen suggereerden. Dat een model in een uur een leesbaar bewijs neerzet, laat zien hoe ver geautomatiseerd redeneren is gekomen. De weegschaal ligt nu bij de wiskundige gemeenschap, en die kijkt naar meer dan of de stappen kloppen: ook naar originaliteit en nette bronvermelding. Zolang de formele controle ontbreekt, is dit een sterke claim en geen vaststaand resultaat. De les zit in het contrast: rekenkracht schaalt makkelijk, vertrouwen niet.