*David> print information
-
We are excited to announce a workshop to bridge the Lean theorem prover and the L-functions and modular forms database (LMFDB), which will be held from Monday, 29 June 2026 to Friday, 3 July 2026 at the University of East Anglia in Norwich, United Kingdom.
This workshop is the first in a series of two workshops for the Scalable Theorem Proving via Mathematical Databases project, funded by the AI for Math Fund managed by Renaissance Philanthropy in partnership with founding donor XTX Markets. The second workshop will be hosted at the Massachusetts Institute of Technology in Cambridge, Massachusetts, United States in early 2027, with more details available by June 2026.
This workshop will feature tutorials to navigate the number theory programming interface in Lean's mathematical library (number fields, elliptic curves, modular forms, etc), as well as a variety of research talks in relevant areas of number theory. The confirmed participants include:
- Alex Best (Harmonic)
- Kevin Buzzard (Imperial College London)
- Riccardo Brasca (Université Paris Cité)
- Richard Hill (University College London)
- David Loeffler (UniDistance Suisse)
- Bhavik Mehta (Imperial College London)
- David Roe (Massachusetts Institute of Technology)
- Jane Shi (Massachusetts Institute of Technology)
- Andrew Sutherland (Massachusetts Institute of Technology)
- Alain Chavarri Villarello (Vrije Universiteit Amsterdam)
- Junyan Xu (Universität Heidelberg)
- Andrew Yang (Imperial College London)
There will be ample working time dedicated to collaborative projects, including formalisation of definitions in the LMFDB as well as projects proposed by participants. We will solicit proposals for lightning talks from participants, and will organise a session if there is enough interest.
We would like to warmly extend invitations to anyone interested in Lean or the LMFDB, but particularly to working arithmetic geometers and the LMFDB community who are curious about formalisation. Due to limited space, registration will be mandatory through our application form by Saturday, 28 February 2026, with some funding for travel and accommodation for early career researchers. While no background in Lean or formalisation will be necessary for participation, it will be immensely helpful to have some interest in the formalisation of number theory or large-scale databases in Lean.
The following is a tentative schedule, with a conference dinner on Thursday evening.
| |
Monday |
Tuesday |
Wednesday |
Thursday |
Friday |
| 0900 -- 1000 |
Registration |
| Tutorial talk |
Research talk |
Research talk |
Research talk |
Research talk |
| 1000 -- 1100 |
| Coffee break |
| 1100 -- 1200 |
Tutorial talk |
Tutorial talk |
Research talk |
Research talk |
Research talk |
| 1200 -- 1300 |
Catered lunch |
| 1300 -- 1400 |
Tutorial talk |
Tutorial talk |
Free afternoon |
Tutorial talk |
Presentations |
| 1400 -- 1500 |
Coffee break |
Coffee break |
| Project work |
Project work |
| 1500 -- 1600 |
| 1600 -- 1700 |
Coffee break |
Coffee break |
| Project work |
Project work |
| 1700 -- 1800 |
and the 