Chatgpt kan autonoom wiskundige bewijzen leveren
VUB-Data Analytics Lab lost met commercieel taalmodel de conjectuur van de wiskundigen Ran en Teng uit 2024 op
Het Data Analytics Lab van de VUB publiceert nieuwe resultaten waaruit blijkt dat het mogelijk is om met commerciële taalmodellen originele wiskundige bewijzen te ontwikkelen. In de publicatie Early Evidence of Vibe-Proving with Consumer LLMs: A Case Study on Spectral Region Characterization with ChatGPT-5.2 (Thinking) tonen de onderzoekers aan dat het commerciële large language model ChatGPT-5.2 (Thinking) van OpenAI zelfstandig een wiskundig probleem kon oplossen.
Het ging in dit concrete geval over een bewijs 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 steeds hetzelfde resultaat geven. Zolang niemand een sluitend bewijs levert, blijft het een conjectuur; zodra het wél bewezen wordt, verandert het in een stelling (theorema).
De studie beschrijft hoe zeven chatsessies met ChatGPT en vier 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 samenvat: “Met het Data Analytics Lab tonen we als één 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 (Postdoctoraal onderzoeker in de onderzoeksgroep Data Analytics Lab 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 herformuleringen van hun trainingdata”, 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 toch nog steeds cruciaal zijn voor de afsluitende controle en het dichten van formele gaten, en dat het proces belangrijk inzicht biedt in waar LLM-assistentie echt een verschil maakt en waar verificatieknelpunten blijven bestaan.
De 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, mits gekoppeld aan menselijk toezicht en kritisch redeneren. "Kandidaat-bewijzen formuleren kan nu veel sneller, maar de bottleneck wordt dan de verificatie door de mens. Dat neemt tijd. Maar ook daar zullen de taalmodellen ons helpen”, besluit VUB-professor Andres Algaba (Data Analytics Lab VUB).
Meer info:
Andres Algaba: andres.algaba@vub.be
De publicatie is vrij beschikbaar via arXiv onder identifier 2602.18918 en biedt een gedetailleerde beschrijving van methode, resultaten en implicaties van deze vroege casestudy in vibe-proving.
