Hiermee wil Dahmen een belangrijke stap zetten in het betrouwbaarder maken van complexe wiskunde. Hij gaat met zijn collega’s werken aan een manier om ingewikkelde wiskundige bewijzen digitaal te controleren. Dat kan uiteindelijk bijdragen aan veiligere software, betere cryptografie en betrouwbaardere AI-systemen.
Bewijsassistenten
Centraal in het project staan zogenoemde bewijsassistenten: softwareprogramma’s die wiskundige stellingen en hun bewijzen in een strikt formele taal controleren. Waar wiskundigen traditioneel vertrouwen op menselijke controle, kan zo’n systeem stap voor stap nagaan of een bewijs klopt. Daardoor wordt het mogelijk om fouten vrijwel volledig uit te sluiten.
Die technologie heeft inmiddels ook praktische toepassingen. Bewijsassistenten worden bijvoorbeeld gebruikt om te controleren of cruciale software – zoals compilers, vliegtuigbesturingssystemen of cryptografische protocollen – echt foutloos werkt. Ook kunnen ze helpen bij het beoordelen van wiskundige resultaten die door kunstmatige intelligentie worden gegenereerd.
Dahmen richt zich op een bijzonder lastig type wiskundige probleem: Diophantische vergelijkingen. Dat zijn polynoomvergelijkingen in gehele getallen, een onderzoeksgebied dat al eeuwen oud is maar nog steeds een centrale rol speelt in de moderne getaltheorie. De oplosmethoden ervan zijn vaak belangrijk voor andere vakgebieden, zoals meetkunde en cryptografie.
“Het probleem is dat modern onderzoek naar deze vergelijkingen een combinatie is van abstracte theorie en geavanceerde computerberekeningen. Juist die berekeningen zijn nog nauwelijks geïntegreerd in de huidige bewijsassistenten. Daardoor is het moeilijk om recente wiskundige resultaten op dit terrein volledig digitaal te verifiëren,” aldus Dahmen.
Certificaat-aanpak
Het team van Dahmen wil die kloof overbruggen. De onderzoekers ontwikkelen nieuwe methoden om zowel de theorie als de benodigde berekeningen in bewijsassistenten onder te brengen. Daarbij gebruiken ze een zogenoemde certificaat-aanpak: externe rekenprogramma’s voeren berekeningen uit, waarna bewijsassistenten automatisch controleren of de resultaten correct zijn. Als dit lukt, ontstaat een digitale bibliotheek waarin belangrijke delen van de moderne getaltheorie formeel zijn vastgelegd. Zulke bibliotheken kunnen door onderzoekers wereldwijd worden gebruikt en uitgebreid.
Volgens Dahmen kan dit de betrouwbaarheid van wiskundige kennis vergroten en deze toegankelijker maken. De impact kan verder reiken dan de academische wereld: dezelfde technieken kunnen bijdragen aan sterkere cryptografie en betrouwbaardere digitale systemen – technologieën die een steeds grotere rol spelen in de samenleving.
Over Sander Dahmen
Sander Dahmen is universitair hoofddocent bij de afdeling Wiskunde. Voordat hij deze Vici-beurs ontving, ontving hij al een Veni- en een Vidi-beurs, naast andere nationale en EU-beurzen. Sommige van deze laatste projecten lopen nog, zoals het Horizon Europe Marie Skłodowska-Curie Doctoral Network COGENT, dat tot doel heeft 13 promovendi op te leiden en waarbij Dahmen als werkpakketleider betrokken is. Hij verbindt graag onderzoek en onderwijs en heeft onlangs een SKO-project afgerond over het opbouwen van een gemeenschap binnen de bacheloropleiding Wiskunde.