Een expertmeeting (middag) over bewijsassistenten in de wiskunde en een publiekssymposium (avond) voer de nieuwste ontwikkelingen op het gebied van AI voor de wiskunde. U bent welkom bij beide bijeenkomsten. De voertaal is Engels.
Ga direct naar: navigatie
Ga direct naar: inhoud
22mei
Bewijzen: van Euclides naar AI - Op zoek naar de kracht van deep learning
Expertmeeting 14 - 17 uur
De afgelopen jaren zijn de ontwikkelingen op het gebied van bewijsassistenten verbazingwekkend snel gegaan, waarbij de aanpak op het gebied van computerondersteund redeneren en verifiëren in de wiskunde drastisch aan het veranderen is. Deze krachtige tools, die zijn ontwikkeld als hulpmiddel bij het ontwikkelen en controleren van formele bewijzen, vinden al significante toepassing – niet alleen in het onderwijs maar ook in baanbrekend onderzoek.
In het onderwijs zijn bewijsassistenten een belangrijk hulpmiddel voor studenten én docenten, waarmee een praktische aanpak ontstaat voor het onder de knie krijgen van formele logica en bewijstechnieken. Dankzij deze assistenten leren studenten op een interactieve manier omgaan met complexe wiskundige concepten en krijgen zo een beter begrip van de materie. Door de studenten te laten experimenteren met bewijzen, waarbij ze onmiddellijk feedback krijgen, stimuleren deze tools niet alleen de leerervaring maar ook het kritisch vermogen van studenten.
Op het gebied van onderzoek zorgen bewijsassistenten voor revolutionaire ontwikkelingen als het gaat om wiskundige ontdekkingen en verificatie. Ze faciliteren de formalisering van complexe theorieën en de verificatie van ingewikkelde bewijzen, wat uiteindelijk leidt tot een grotere mate van nauwkeurigheid en betrouwbaarheid in wiskundig onderzoek. Onderzoekers werken constant aan de verbetering van deze tools om uitdagende problemen op te lossen, samenwerking tussen disciplines te stimuleren en de grenzen van de mogelijkheden binnen de wiskunde te verleggen.
De drie sprekers van deze middag gaan in op de gevolgen die deze tools hebben voor onderwijs en onderzoek, waarbij ze inzoomen op de ontwikkelingen die medebepalend zijn voor de toekomst van de wiskunde. Onderdeel van de plenaire discussie is een Q&A-sessie, waarbij het publiek vragen kan stellen aan de deskundigen met betrekking tot hun ervaringen met het gebruik van bewijsassistenten in de wiskunde.
Programma
13.30 uur – Registratie, koffie & thee
13.55 uur – Woord van welkom en inleiding door Jan van Neerven, lid van de KNAW, hoogleraar wiskunde aan de Technische Universiteit Delft
14.00 uur – María Inés de Frutos Fernández, postdoc-onderzoeker Formal Mathematics, Universiteit Bonn– The Carleson project: a collaborative formalization
14.45 uur – Johannes Schmitt, postdoc-onderzoeker Mathematics, Algebraic geometry, ETH Zurich – Large Language Models in Mathematics - the Profane and the Sacred
15.30 uur – Jim Portegies, universitair docent bij de Applied Analysis-groep van het Center for Analysis, Scientific computing and Applications (CASA) van de TU Eindhoven (TU/e) – ‘Waterproof’ and how to use formal mathematics in education
16.15 uur – Plenaire vragen en discussie
17.00 uur – Afsluiting en borrel
Symposium 19 - 21 uur
In 2024 verraste DeepMind de wereld toen het aankondigde dat hun AlphaProof AI-systeem een zilveren medaille had behaald op de Internationale Wiskunde Olympiade. Hoewel wetenschappers al sinds de opkomst van de eerste computers dromen van computers die stellingen bewijzen, lijkt dit vooruitzicht nu steeds realistischer te worden.
Wij nodigen u graag uit voor een symposium dat de geschiedenis en toekomst van het wiskundig bewijs zal verkennen. Hoe kunnen computers stellingen bewijzen? Hoe kunnen we zeker weten dat die bewijzen correct zijn, en niet het resultaat van een ‘hallucinatie’? Zien we binnenkort een AI een van de grote open problemen in de wiskunde oplossen?
De sprekers praten u bij over de nieuwste ontwikkelingen op het gebied van AI voor de wiskunde. Of u nu wiskundige of informaticus bent, of gewoon nieuwsgierig naar de toekomst van technologie - dit symposium belooft te inspireren en te verhelderen.
Programma
18.30 uur – Registratie, koffie & thee
18.55 uur – Woord van welkom en inleiding door Jan van Neerven, lid van de KNAW, hoogleraar wiskunde aan de Technische Universiteit Delft
19.00 uur – Catarina Dutilh Novaes,hoogleraar Reasoning and Argumentation aan de Vrije Universiteit Amsterdam – The Dialogical Roots of Mathematical Proof
19.30 uur – Johan Commelin, universitair docent Fundamental Mathematics aan de Universiteit Utrecht, en bij Lean FRO – Can we trust computers doing maths?
20.00 uur – Oliver Nash, wiskundige, ex-DeepMind, Universiteit van Dublin, Ierland – DeepMind's AlphaProof and AI-generated mathematics
20.30 uur – Plenaire vragen en discussie
21.00 uur – Afsluiting en borrel