Topwiskundigen vragen AI-bedrijven om meer aandacht voor begrip

Vijfentwintig winnaars van de Fieldsmedaille vragen AI-bedrijven om hun aanpak van wiskundig onderzoek te veranderen. Terence Tao publiceerde hun gezamenlijke verklaring op 11 september. Volgens de ondertekenaars krijgt het snel oplossen van moeilijke problemen te veel nadruk, terwijl uitleg, nieuwe inzichten en de opleiding van onderzoekers juist tijd en aandacht nodig hebben.

De groep ziet ook kansen voor AI. Hun bezwaar is dat snelle aankondigingen van oplossingen het zorgvuldig uitwerken en doorgeven van ideeën kunnen verdringen. Ze vragen om overleg tussen wiskundigen, technologiebedrijven en de samenleving over wat onderzoek uiteindelijk moet opleveren.

Hoe een computer een bewijs controleert

Er bestaat een belangrijk verschil tussen het bedenken en het controleren van een bewijs. Lean, een programmeertaal en bewijsassistent, maakt dat onderscheid concreet. Volgens de eigen documentatie worden bewijsscripts omgezet in een expliciet bewijsobject: een precies geformuleerde redenering in de onderliggende logica. Vervolgens controleert een klein onderdeel van de software, de kernel, of dat bewijs aan de regels voldoet. Het systeem beoordeelt daarmee meer dan alleen een eindantwoord.

Die scheiding betekent dat de betrouwbaarheid van de controle niet hoeft af te hangen van iedere methode waarmee het bewijs werd gevonden. Lean beschrijft bovendien hoe bewijsobjecten kunnen worden geëxporteerd en door een afzonderlijke controleur worden nagekeken, eventueel op een andere computer. De betrouwbaarheid van die controleur blijft wel een aanname. Meerdere onafhankelijke controleurs kunnen volgens de documentatie het vertrouwen verder vergroten.

Een wedstrijdscore heeft voorwaarden

Google DeepMind liet in juli 2024 al zien hoe zulke technieken in AI-onderzoek worden gebruikt. AlphaProof zocht naar bewijzen in Lean en gebruikte gevonden, gecontroleerde bewijzen om verder te leren. Samen met AlphaGeometry 2 loste het volgens DeepMind vier van de zes opgaven van de Internationale Wiskunde Olympiade op. De behaalde 28 punten kwamen overeen met het niveau voor een zilveren medaille.

Bij die vergelijking hoorden belangrijke voorwaarden. Mensen hadden de wedstrijdopgaven eerst naar formele wiskundige taal vertaald. Waar scholieren twee sessies van 4,5 uur kregen, hadden de systemen voor sommige oplossingen tot drie dagen nodig. Dit voorbeeld uit 2024 illustreert waarom een score en de omstandigheden samen moeten worden gelezen: dezelfde puntentelling betekent nog niet dezelfde werkwijze of tijdslimiet.

Eerdere oproep uit Leiden

De nieuwe verklaring sluit aan bij een bredere discussie. De Leiden Declaration, gepubliceerd op 2 juni 2026, bevat al concrete aanbevelingen voor onderzoekers en organisaties. Daarin staat dat ook een formeel bewijs een aandachtspunt overlaat: de vertaling tussen de computerbeschrijving en het probleem zoals mensen dat bedoelen. De auteurs waarschuwen dat problemen in die vertaalslag de beoordeling van een resultaat ingewikkelder kunnen maken.

De Leidse verklaring vraagt onderzoekers daarom te vermelden welke hulpmiddelen zij gebruiken, nauwkeurig naar eerder werk te verwijzen en zelf verantwoordelijkheid te houden voor correctheid. Voor organisaties noemt zij onder meer menselijke uitleg van de centrale redenering en formele controle waar die passend is. Publicatie in wetenschappelijke tijdschriften en beoordeling door vakgenoten blijven volgens de opstellers nodig. Een persbericht kan daarbij helpen, maar vervangt die controle niet.