# Topwiskundigen vragen AI-bedrijven om meer aandacht voor begrip Een verklaring van 25 Fieldsmedaillewinnaars vraagt ruimte voor uitleg en opleiding. Hoe verhouden AI-antwoorden, gecontroleerde bewijzen en menselijk begrip zich tot elkaar? - Canonieke URL: https://ngnews.nl/artikel/topwiskundigen-vragen-ai-bedrijven-om-meer-aandacht-voor-begrip - Gepubliceerd: 2026-09-13T00:36:24Z - Rubriek: Tech - Uitgever: Nxt ![AI-illustratie van een rode tekenpasser boven een meetkundige tekening, verbonden met een computerchip.](https://ngnews.nl/web/images/nxt-ce3ab55feddc6079b6d8.jpg) AI-illustratie · Nxt Generation News · Geen foto van de beschreven gebeurtenis. 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. Bronnen bij deze passage: [1. Terence Tao — verklaring van 11 september](https://terrytao.wordpress.com/2026/09/11/a-severe-misalignment-of-ai-in-mathematics/) 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. Bronnen bij deze passage: [1. Terence Tao — verklaring van 11 september](https://terrytao.wordpress.com/2026/09/11/a-severe-misalignment-of-ai-in-mathematics/) ## 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. Bronnen bij deze passage: [3. Lean — uitleg over bewijscontrole](https://lean-lang.org/faq/) 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. Bronnen bij deze passage: [3. Lean — uitleg over bewijscontrole](https://lean-lang.org/faq/) ## 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. Bronnen bij deze passage: [4. Google DeepMind — AlphaProof bij de IMO van 2024](https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/) 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. Bronnen bij deze passage: [4. Google DeepMind — AlphaProof bij de IMO van 2024](https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/) ## 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. Bronnen bij deze passage: [2. Leiden Declaration — aanbevelingen voor onderzoekers](https://leidendeclaration.ai/) 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. Bronnen bij deze passage: [2. Leiden Declaration — aanbevelingen voor onderzoekers](https://leidendeclaration.ai/) ## Bronnen - [1. Terence Tao — verklaring van 11 september](https://terrytao.wordpress.com/2026/09/11/a-severe-misalignment-of-ai-in-mathematics/) - [2. Leiden Declaration — aanbevelingen voor onderzoekers](https://leidendeclaration.ai/) - [3. Lean — uitleg over bewijscontrole](https://lean-lang.org/faq/) - [4. Google DeepMind — AlphaProof bij de IMO van 2024](https://deepmind.google/blog/ai-solves-imo-problems-at-silver-medal-level/) [Bronnen en werkwijze](https://ngnews.nl/bronnen#werkwijze)