An expert meeting (afternoon) and a symposium (evening) for a broader public.
An expert meeting (afternoon) and a symposium (evening) for a broader public.
María Inés de Frutos Fernández, Postdoctoral Researcher on Formal Mathematics, Universität Bonn – The Carleson project: a collaborative formalization
In 1966, Lennart Carleson published a proof of an important theorem in harmonic analysis that states that the Fourier series converges pointwise to the original function under weak conditions. All known proofs of this fundamental result are notoriously difficult.
In this talk, I will describe an ongoing project, led by Floris van Doorn, to formalize a complete proof of a recent generalization of Carleson's theorem in the theorem prover Lean. The talk will focus on the collaborative nature of this formalization.
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: transforming a proof assistant into an educational tool
In this talk we demonstrate the educational software Waterproof, that is designed to help students acquiring the skill of writing mathematical proofs. We illustrate the main features of the software, explain how we use it in class and share results of our educational evaluation of the tool.
Johannes Schmitt, Postdoctoral Researcher in Mathematics, Algebraic geometry, ETH Zurich – Large Language Models in Mathematics - the Profane and the Sacred
Since the introduction of the first version of ChatGPT in 2022, AI assistants based on Large Language Models (LLMs) have made lots of progress in cognitive tasks, including mathematical reasoning. After a brief general introduction to LLMs, I'll discuss how they can be useful to the working mathematician, both for mundane tasks (like writing lecture notes or doing literature search) and for mathematical research itself. I'll give an overview both of recent advances and persistent challenges in using LLMs to find proofs.
Catarina Dutilh Novaes, Full Professor, Reasoning and Argumentation at the VU Amsterdam – The Dialogical Roots of Mathematical Proof
In this talk, I will present some of the main findings of my research on the history and philosophy of mathematical proof, in particular as presented in my book The Dialogical Roots of Deduction(2020). In the talk, I will present a conceptual model of mathematical proof in terms of dialogues involving two characters, Prover and Skeptic. I then show how the model can be used to investigate the dialogical origins of mathematical proof in ancient Greece as well as the recent practices of proof in mathematics. While this dialogical nature of proofs has remained influential and stable for millennia, it may now change in view of recent developments in computational mathematics.
Johan Commelin, assistant professor Fundamental Mathematics at Utrecht University, and at the Lean FRO– Can we trust computers doing maths?
Mathematics is built on the ideal of absolute rigor-proofs that, in principle, leave no room for doubt. In this talk, I explore how computers can help realize this ideal by verifying the correctness of mathematical arguments. This opens new possibilities for large-scale collaboration between mathematicians and AI systems. But even with such tools, can we truly eliminate the need for trust? I’ll reflect on what this means for the practice of mathematics today and in the future.
Oliver Nash, Mathematician, ex-DeepMind – DeepMind's AlphaProof and AI-generated mathematics
In July 2024, a seminal event for mathematics and for AI took place. For the first time ever, an AI agent competed in the International Mathematics Olympiad. Moreover this agent, known as AlphaProof, did not just compete: it matched or surpassed the performance of more than 90% of human contestants. As a former member of the team which built AlphaProof, I will explain what this means, outline some of the means by which this achievement was made possible, and speculate on what I think AI can do for mathematics in the near future.
An expert meeting (afternoon) and a symposium (evening) for a broader public.
View meeting