An expert meeting (afternoon) and a symposium (evening) for a broader public. You are welcome to attend both meetings.
Go directly to: navigation
Go directly to: content
Expert meeting 2 - 5 p.m.
In recent years, the field of computer proof assistants has witnessed remarkable advancements, transforming the way we approach mathematical reasoning and verification. These powerful tools, designed to assist in the development and checking of formal proofs, have found significant applications in both educational settings and cutting-edge research.
In education, proof assistants serve as invaluable resources for students and educators alike, providing a hands-on approach to learning formal logic and proof techniques. They enable learners to engage with complex mathematical concepts in an interactive manner, fostering a deeper understanding of the subject matter. By allowing students to experiment with proofs and receive immediate feedback, these tools enhance the learning experience and encourage critical thinking.
On the research front, computer proof assistants are revolutionizing the landscape of mathematical discovery and verification. They facilitate the formalization of complex theories and the verification of intricate proofs, ensuring a higher level of rigor and reliability in mathematical work. Researchers are increasingly leveraging these tools to tackle challenging problems, collaborate across disciplines, and push the boundaries of what is possible in mathematics.
The three speakers of this afternoon will explore their impact on education and research, highlighting the exciting developments that are shaping the future of mathematics. During the discussion session, we will incorporate a Q&A session where the audience can ask domain experts about their experience with the use of proof assistants in mathematics.
Programme
1.30 p.m. Registration, coffee & tea
1.55 p.m. Welcome and introduction by Jan van Neerven, Academy member, Professor of Mathematics, Delft University of Technology
2.00 p.m. María Inés de Frutos Fernández, Postdoctoral Researcher on Formal Mathematics, Universität Bonn – The Carleson project: a collaborative formalization
2.45 p.m. Johannes Schmitt, Postdoctoral Researcher in Mathematics, Algebraic geometry, ETH Zurich – Large Language Models in Mathematics - the Profane and the Sacred
3.30 p.m. Jim Portegies, Assistant Professor in the Applied Analysis group of the Centre for Analysis, Scientific computing and Applications (CASA) at Eindhoven University of Technology (TU/e) – ‘Waterproof’ and how to use formal mathematics in education
4.15 p.m. Plenary questions and discussion
5.00 p.m. Closure and drinks
As of 7.00 p.m. a symposium open for a broader public with specific interest in this field of research will be held in the Tinbergen Zaal at the KNAW.
Symposium 7 - 9 p.m.
In 2024 Deepmind took the world by surprise when they announced that their AlphaProof AI system had obtained a silver-medal winning performance at the International Mathematical Olympiad. Although scientists have dreamt of computers proving theorems since the advent of the very first computers, this prospect is now becoming increasingly realistic.
We are delighted to invite you to a symposium that will explore the history and future of mathematical proof. How can computers prove theorems? How can we make sure they are correct, and not ‘hallucinating’? Will we soon see an AI solving one of the big open problems in mathematics?
The speakers will inform you about the latest advances in AI for mathematics. Whether you are a mathematician, computer scientist, or simply curious about the future of technology, this symposium promises to inspire and enlighten.
Programme
6.30 p.m. Registration, coffee & tea
6.55 p.m. Welcome and introduction by Jan van Neerven, Academy member, Professor of mathematics, Academy member, Delft University of Technology
7.00 p.m. Catarina Dutilh Novaes, Full Professor, Reasoning and Argumentation at the VU Amsterdam – The Dialogical Roots of Mathematical Proof
7.30 p.m. Johan Commelin, assistant professor Fundamental Mathematics at Utrecht University, and at the Lean FRO– Can we trust computers doing maths?
8.00 p.m. Oliver Nash, Mathematician, ex-DeepMind, University of Dublin Ireland – DeepMind's AlphaProof and AI-generated mathematics
8.30 p.m. Plenary questions and discussion
9.00 p.m. Drinks