Wiskundige verwerpt OpenAI's conjectuur-doorbraak binnen 24 uur: 'AI bewees elke zin, maar het gaat niet meer over de oorspronkelijke conjectuur'

OpenAI beweerde dat zijn nieuwste AI-model tien wereldklasse wiskundeproblemen oploste, waaronder het weerleggen van het vermoeden van Connes over starheid. De volgende dag reageerde een menselijke wiskundige met een artikel waarin zij stelt dat het tegenvoorbeeld van de AI ongeldig is. De auteur, J. L. Nielsen van het Topology Physics Center van de Universiteit van Kansas, volgde de 37.000 regels Lean 4-code van OpenAI van begin tot eind, bracht elk object terug naar zijn wiskundige prototype en identificeerde twee onafhankelijke foutpaden. Het vermoeden van Connes over starheid stelt dat als twee groepen dezelfde geassocieerde algebraïsche structuur hebben en aan twee aanvullende voorwaarden voldoen (ICC en Kazhdan's eigenschap (T)), de groepen dan isomorf moeten zijn. OpenAI's model construeerde twee niet-isomorfe groepen die dezelfde algebra genereren, met bewijzen dat beide groepen aan ICC en eigenschap (T) voldoen. Nielsen wees erop dat een van de door AI geconstrueerde groepen in feite niet aan de aanvullende voorwaarden voldeed, omdat deze noch ICC noch eigenschap (T) had. Ze noemde drie mogelijke redenen: de representatie van eigenschap (T) in de code kwam niet getrouw overeen met de oorspronkelijke definitie van Kazhdan; het bewijs gold slechts voor een deel van de groep maar werd toegepast op de hele groep; of de groep in de code is niet wat het verklarende document beschrijft. Nielsen voerde ook een regel-voor-regelcontrole van de code uit en zette de naam en het regelnummer van elk wiskundig object in een kruisverwijzingstabel. Ze ontdekte dat de lemma's die werden gebruikt om ICC te bewijzen, van toepassing waren op objecten na een duale transformatie, niet op de oorspronkelijke groep met zijn centrale elementen, dus ze dekten de kritieke elementen niet direct. Ze schreef haar twee weerleggingen als Lean-code en compileerde ze onder Lean 4.32.2. Het laatste deel van het artikel bespreekt de bredere context: de Lean-kernel garandeert formele correctheid, maar niet of de verklaring daadwerkelijk de bedoelde conclusie bewijst. Terence Tao citerend: het verifiëren van een bewijs controleert de formele verklaring zelf, niet de overeenstemming met de bedoeling, dus menselijke beoordeling kan niet worden vervangen. Eerdere audits van vijf gangbare Lean-benchmarks vonden 4.833 problemen, waaronder tegenvoorbeelden, lege stellingen en onbetrouwbare axioma's, allemaal machine-geverifieerd, waarbij mensen later tegenvoorbeelden construeerden om aan te tonen dat de bewezen stellingen onjuist waren. Nielsen schreef dat OpenAI's formalisering mogelijk elke conclusie die het beweert correct heeft vastgesteld, maar wat het niet heeft vastgesteld - en wat de Lean-kernel niet kan controleren - is of deze conclusies verband houden met de formulering van het oorspronkelijke vermoeden. Het vermoeden van Connes over starheid blijft open.