ChatGPT levert autonoom wiskundig bewijs

ChatGPT is erin geslaagd om een bewijs te leveren dat een conjectuur uit 2024 van de wiskundigen Ran en Teng verklaart. Een conjectuur is een bewering waarvan men denkt dat ze waar is, omdat er veel voorbeelden of aanwijzingen voor zijn, maar waarvoor nog geen formeel bewijs bestaat. Wiskundigen formuleren zo’n vermoeden vaak nadat ze een patroon hebben ontdekt of na veel berekeningen die altijd hetzelfde resultaat geven. Zolang niemand een sluitend bewijs levert, blijft het een conjectuur; zodra het wél bewezen wordt, verandert het in een stelling of theorema.

De studie beschrijft hoe 7 chatsessies met ChatGPT en 4 versies van het bewijs gezamenlijk het uiteindelijke bewijs opleverden. ChatGPT bleek met name nuttig bij de zoektocht naar het bewijs, terwijl menselijke experts essentieel waren voor de correctheidscontrole en de sluitende argumentatie. 

De auteurs tonen aan dat ChatGPT-5.2 (Thinking) de structuur van het bewijs grotendeels zelf ontwikkelde, met minimale menselijke tussenkomst. Zoals de korte beschrijving van de paper het samenvat: “Met het Data Analytics Lab tonen we als een van de eerste aan dat een commercieel beschikbaar LLM zelfstandig originele wiskundige bewijzen kan ontwikkelen.”  

"Ik had al langer het vermoeden dat ChatGPT me kon helpen bij het bewijs van onopgeloste wiskundige problemen", zegt Brecht Verbeken, postddoctoraal onderzoeker in de onderzoeksgroep Data Analytics Lab van de VUB. “En toch was ik verbaasd hoe efficiënt dat verliep.” 

De onderzoekers plaatsen hun werk in de bredere context van wat zij vibe-proving noemen, een benadering waarbij taalmodellen worden ingezet om theoretische redeneringen op hoog niveau te verkennen en te structureren. De kernvraag in de publicatie is of die vibe-proving-techniek het komende jaar eenzelfde snelle evolutie zal doormaken als eerder gezien bij AI-geassisteerd programmeren (vibe-coding), waarbij systemen zich ontwikkelden van hulpmiddel tot vrijwel autonome codegenerator. "We horen vaak hoe mensen denken dat de creativiteit van de systemen fundamenteel beperkt blijft tot het herformuleren van trainingsdata”, zegt VUB-professor Vincent Ginis (Data Analytics Lab). “Blij dat we ook dat misverstand met ons werk kunnen weerleggen…”  

De auteurs benadrukken dat, hoewel het model een substantieel deel van het bewijsschema zelf genereerde, mensen nog steeds cruciaal zijn voor de afsluitende controle en het dichten van formele gaten. Het proces toont vooral duidelijk aan waar LLM-assistentie echt het verschil maakt en waar verificatieknelpunten blijven bestaan. Deze ontwikkeling markeert een belangrijk moment in de inzet van AI binnen theoretisch onderzoek: niet alleen als hulp bij programmeren en tekstproductie, maar als instrument dat kan bijdragen aan originele wiskundige ontdekkingen. Al moet dat nog altijd gekoppeld worden aan menselijk toezicht en kritisch redeneren. "Kandidaat-bewijzen formuleren kan nu veel sneller, maar de bottleneck wordt dan de verificatie door de mens. Dat vergt tijd. Maar ook daar zullen de taalmodellen ons vast helpen,” besluit VUB-professor Andres Algaba (Data Analytics Lab VUB).