Description
AIMM (AI Meets Mathematics) is a workshop about AI in mathematics, held at Imperial College London (White City Campus), 28-29 Aug 2025. All are welcome!
Registration
Registrations are now closed.
Schedule
| Time | Thu, 28 Aug 2025 | Fri, 29 Aug 2025 |
|---|---|---|
| 9.30-10.00 | Registration | |
| 10.00-11.00 |
Kevin Buzzard (Talk) |
Adam Zsolt Wagner (Talk) |
| 11.30-12.30 |
Challenger Mishra, Kevin Buzzard, Yang-Hui He, Al Kasprzyk (Panel discussion) |
Bhavik Mehta (Tutorial) |
| 12.30-14.00 | Lunch | Lunch |
| 14.00-15.00 |
Roan Talbut (Talk) |
Felix Schremmer (Talk) |
| 15.30-16.30 |
Ed Hirst (Talk) |
Thomas Oliver (Talk) |
Abstracts
Kevin Buzzard (Imperial College London): AI and reasoning
I will explain my possibly ill-informed views on AI's abilities to reason at research level, and will go on to talk about two projects which I’m involved in, which are attempts to make their reasoning abilities more powerful by offering them data formalised in the Lean theorem prover.
Adam Zsolt Wagner (Google DeepMind): Finding interesting mathematical objects with ML methods
I will talk about various ML tools we can use today to try to find interesting constructions to various mathematical problems. These will range from very simple reinforcement learning programs to LLM-based tools such as AlphaEvolve. We will discuss the pros and cons of several of these methods, and try to figure out which one is best for the problems you care about.
Bhavik Mehta (Imperial College London): A hands-on introduction to the Lean Theorem Prover
This talk offers a practical introduction to the Lean Theorem Prover, designed for both mathematicians and AI researchers. Through a live demonstration, we will illustrate the interactive process of writing definitions, stating theorems, and constructing proofs in Lean. Building on this, we will discuss the synergy between Lean and AI, exploring recent advancements such as machine learning-based tools for proof search and tactic suggestion.
Roan Talbut (Imperial College London): Tropical Gradient Descent
In this talk, I will introduce tropical geometry - a variant of algebraic geometry which provides a geometric lens through which to view non-smooth optimisation problems, and that has become increasingly studied in applications such as computational biology, economics, and computer science. We will review various types of convexity which arise in tropical problems, and we propose a new gradient descent method for solving tropical optimisation problems. Theoretical results establish global solvability for tropically quasi-convex problems, while numerical experiments demonstrate the method's superior performance over classical descent for tropical optimisation problems which exhibit tropical quasi-convexity but not classical convexity. Notably, tropical gradient descent seamlessly integrates into advanced optimisation methods, such as Adam, offering improved overall performance.
Felix Schremmer (University of Hong Kong): Machine learning assisted exploration for affine Deligne–Lusztig varieties
In this interdisciplinary study, we describe a procedure to assist and accelerate research in pure mathematics by using machine learning. We study affine Deligne–Lusztig varieties, certain geometric objects related to a number of mathematical questions, by carefully developing a number of machine learning models. This iterated pipeline yields well interpretable and highly accurate models, thus producing strongly supported mathematical conjectures. We explain how this method could have dramatically accelerated the research in the past. A completely new mathematical theorem, found by our ML-assisted method and proved using the classical mathematical tools of the field, concludes this study. This is joint work with Bin Dong, Pengfei Jin, Xuhua He and Qingchao Yu.
Ed Hirst (Queen Mary University of London): AInstein: Numerical Einstein Metrics via Machine Learning
A semi-supervised framework for finding and modelling Einstein metrics as neural networks is presented, based on a loss term which is the Einstein condition. The framework is validated for solving the vacuum Einstein equations with a cosmological constant on spheres of varying dimension. Ongoing work is discussed where the framework is applied to geometries with Lorentzian signature, including search for the Schwarzschild solution.
Thomas Oliver (University of Westminster): Murmurations: heuristic and rigorous perspectives
Murmurations are statistical correlations between Frobenius traces and root numbers. Although they were discovered with heuristic methods, they are now a topic of rigorous research. In this talk, I will offer some arithmetic context and outline the data-driven discovery.
Location
The workshop is held in the Translation & Innovation Hub, 84 Wood Ln, London W12 0BZ, 5th floor. This is on the White City campus of Imperial College London and not in South Kensington. The nearest underground stations are White City (Central Line) and Wood Lane (Circle and Hammersmith and City line).
Contact
In case of questions, please contact Elli Heyes or Sara Veneziale or Daniel Platt.
Sponsors
The event is being funded/sponsored by the IX Centre for AI in Science, supported by Schmidt Sciences. We gratefully acknowledge their support.