De voorbije dagen wees Terence Tao erop dat er op de Erdős Problems-website een mijlpaal is bereikt: een open probleem van Erdős (nummer #728) kreeg een oplossing waarbij AI-tools een opvallend grote rol speelden — en de kernstelling werd bovendien formeel geverifieerd in Lean.

Lean is een bewijsassistent : software waarmee je wiskundige definities, stellingen en bewijzen zó precies opschrijft dat de computer stap voor stap kan controleren of alles logisch klopt.

Wat doet Lean concreet?

• Het definieert objecten: groepen, ringen, verzamelingen, limieten, enz.

• Het formuleert een stelling in formele taal.

• Het schrijft een bewijs als een reeks kleine logische stappen (tactieken of termen).

• Lean accepteert het bewijs alleen als elke stap geldig is volgens de logica én volgens de eerder gedefinieerde begrippen.

Als Lean “QED” bereikt, betekent dat: het bewijs is formeel correct binnen het systeem.

De status op de probleem-pagina is ondertussen:

PROVED (LEAN) – opgelost en het bewijs is in Lean geverifieerd.

Concreet vermeldt de pagina dat Kevin Barreto en ChatGPT-5.2 bewezen hebben dat er (zelfs vrij “symmetrische”) oplossingen bestaan. 

En wat is nu juist de rol geweest van Chatgpt?

1. Een informeel argument werd gegenereerd met een taalmodel (GPT-5.2/ChatGPT-5.2).

2. Dat argument werd vervolgens geformaliseerd in Lean met hulp van een automatische formaliserings-/theorem-proving tool (“Aristotle” wordt expliciet genoemd), waarna anderen konden nakijken of de formele statement klopt.

3. Daarna volgden er menselijke controles: klopt de formulering, hoe zit het met trivialiteiten, en is er eerdere literatuur (bv. Pomerance) die verwant is?

Dat laatste is cruciaal: een Lean-check geeft heel veel zekerheid dat de formele proof correct is voor de exacte formele stelling — maar je wil nog steeds menselijke zorg voor (i) interpretatie van het “bedoelde” probleem en (ii) correcte situering in bestaande literatuur. 

In de thread maakt Tao een  heel didactisch punt: wiskunde gaat niet enkel om een proof-object, maar om begrip. Een AI kan een technisch correcte redenering produceren, maar het “rondmaken” — motivering, context, why-this-works, verbanden met eerdere resultaten — blijft essentieel. AI speelde een hoofdrol in het produceren van een bruikbaar argument en in (semi-)automatische formaliseringsstappen, maar het geheel gebeurde in een community-proces met menselijke controle, discussie over interpretatie, en aandacht voor literatuur.