Programme
Talks will be held in the Auditorium on Monday, and in the Blue Room on Tuesday and Wednesday.
Schedule
Abstracts:
María Inés de Frutos Fernández (Universität Bonn):
- Tittle: Mathematical formalization with Lean 4
- Abstract: Mathematical formalization consists of digitizing mathematical definitions, statements and proofs, using a special kind of software known as a proof assistant or theorem prover. This course will be an introduction to formalization using the interactive theorem prover Lean, which has become very popular among mathematicians due to both its extensive mathematical library, Mathlib, and several large formalization projects using this prover, including the Liquid Tensor Experiment, the Polynomial Freiman–Ruzsa Conjecture, the Carleson project, and the optimal sphere packing in dimensions 8 and 24. We will familiarize ourselves with Lean and Mathlib by formalizing examples from several areas of mathematics, including logic, algebra, calculus, and topology.
The course assumes no previous experience with formalization. Participants are kindly asked to install Lean before the first lecture by following the instructions at https://lean-lang.org/install/
Damien Galant (Brown University):
- Tittle: Artificial intelligence for the working mathematician
- Abstract: Machines have been doing mathematics for seventy years. They have explored, computing the examples from which we conjecture, from Riemann's zeros and Turing's machinery to Fermi-Pasta-Ulam-Tsingou and the conjectures that died of a counterexample. They have verified, checking case analyses no human will ever read, from the four colour theorem to interval arithmetic and modern SATsolvers. What is new is a third role: the machine as collaborator.
This course is a working mathematician's report on that third role -- what the current systems are, what they do well, where their limits lie, and what discipline their use requires. It is addressed to mathematicians with no particular interest in artificial intelligence and every interest in the problems they already work on. No background in machine learning is assumed; what is needed to judge the claims will be supplied.
We begin with the history, computer-assisted exploration and computer-assisted proof, neither of which needed AI, and with what neural networks and language models actually are in terms a mathematician can check: an approximation class, a regression problem, and a next-token predictor that turned out to scale. The middle of the course is practical and largely live -- agents that read, compute and write code, tools built for a single problem, and evolutionary search over programs. We close with what all this does to our community: disclosure, reproducibility, refereeing, the fact that mathematics now has a budget, and how we train students.
Mitchell Taylor (Oxford University):
- Tittle: Autofomalization and discovery in analysis and PDE
- Abstract: I will discuss some new opportunities provided by AI in mathematics. The main one is formalization in Lean, and I will try to explain how this is now entirely within reach and that any paper in analysis and PDE can now be fully formalized.