ENGINEERINGNET.BE - In hun publicatie (*) 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.
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 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.
(*) Early Evidence of Vibe-Proving with Consumer LLMs: A Case Study on Spectral Region Characterization with ChatGPT-5.2 (Thinking)
