Doorbraak in wiskunde? AI-systeem “Aristotle” van Harmonic claimt oplossing voor 30-jaar oud Paul Erdős-probleem
Het AI-systeem Aristotle zou, geheel autonoom, een versie van het al decennia openstaande Erdős Problem #124 hebben bewezen en de oplossing formeel geverifieerd in de formaliseringstaal Lean. Dit markeert volgens de makers het begin van een nieuw tijdperk in wiskunde: “vibe proving”, waarin AI-gedreven ontdekking en machine-verifieerbare rigor samenkomen.
Wat is er gebeurd
Harmonic, mede opgericht door Vlad Tenev, kondigde aan dat Aristotle binnen zes uur een versie van Erdős Problem #124 oploste, en binnen een minuut de compacte formele bewijscode in Lean genereerde.
Volgens Harmonic draait Aristotle’s architectuur op een combinatie van informele “mens-achtige” redenering en formele verificatie: het zoekt en structureert lemmas in natuurlijke taal, zet die om naar Lean en genereert zo volledig machine-controleerbare bewijzen.
Eerder dit jaar behaalde Aristotle al “gold-medal level” prestaties op de 2025 International Mathematical Olympiad (IMO) door 5 van de 6 problemen correct op te lossen met formeel bewijs.
Wat betekent “een versie van het probleem opgelost”
Belangrijk: onderzoekers benadrukken dat Aristotle niet per se de “originele en moeilijkste” versie van probleem #124 heeft opgelost, maar een makkelijker of vereenvoudigde variant.
Volgens de beheerder van de database met Erdős-problemen: “Aristotle loste ‘een’ versie op van dit probleem (effectief met een olympiad-stijl bewijs), maar niet ‘dé’ versie.”
De originele, krachtiger geformuleerde conjectuur, met strengere voorwaarden (zoals extra gcd-condities), blijft volgens hem openstaan.
Enkel omdat de AI-bewijzen formeel zijn geverifieerd in Lean, is het resultaat inderdaad correct voor de versie die wordt bewezen. Dat impliceert echter niet dat alle varianten van het oude probleem hiermee afgevinkt zijn.
Waarom dit toch een belangrijke ontwikkeling is
Het is een van de eerste keren dat een AI-systeem volledig zelfstandig beweert te slagen in een wiskundig probleem dat gemeld stond als “decennia open”. Daarmee gaat AI verder dan enkel hulp bij menselijk werk: het levert autonoom “nieuw” wiskundig werk.
De combinatie van natuurlijke taal-redenering + machine-verifieerbare output toont dat wiskundige creativiteit + rigor op grote schaal geautomatiseerd kunnen worden. Dit opent de deur naar veel snellere exploratie van conjecturen, en maakt formele wiskunde toegankelijker buiten elite-kringen.
Zelfs als het om “lager hangend fruit” gaat (makkelijker varianten), illustreert het het potentieel van wat we soms “wiskundige superintelligentie” noemen, AI die niet alleen assisteert, maar ook origineel produceert.
Waarom sommigen kritisch blijven
Niet iedereen is even enthousiast:
Zoals gezegd: het ging om een vereenvoudigde varianten, niet de strengere originele conjectuur.
Sommige wiskundigen wijzen erop dat de oplossing in retrospectief “eenvoudig” is, alsof men in een wiskundecompetitie zit. Dat roept de vraag op: zou deze “armoedige” variant niet al eerder ontdekt zijn?
Mensen die kritisch staan tegenover wat nu “AI-hype” noemen, benadrukken dat er al langer automatische bewijs-assistenten bestaan, en dat echte vooruitgang pas komt wanneer AI nieuwe, fundamentele conjecturen bedenkt, niet alleen bestaande oplost.
Wat dit betekent voor de toekomst van wiskunde
We staan mogelijk aan de vooravond van een paradigmaverschuiving: AI-systemen als Aristotle kunnen flink het tempo en bereik van wiskundig onderzoek versnellen. En niet alleen door menselijke wiskundigen te assisteren, maar ook door autonoom originele bewijzen te produceren.
Formele wiskunde en verificatie (via Lean of vergelijkbare proof assistants) kunnen veel toegankelijker worden. In plaats van complexe, menselijke peer-review kan AI snel rigoureuze validatie doen, waardoor wiskunde minder “elitair” en meer open wordt.
Tegelijk is er nood aan kritische evaluatie: niet alle “oplossingen” betekenen dat alle open vragen beantwoord zijn. Wiskundige traditie en nuance blijven cruciaal, ook in een tijdperk van “vibe proving”.