and 
This workshop is the second 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 first workshop in the series was hosted at the University of East Anglia in Norwich, England from June 29 to July 3, 2026.
|
Confirmed participants |
Depending on participant interest, this workshop may 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. We hope to continue the progress made in the first workshop, developing Lean tactics and certificates for proving the correctness of LMFDB data. There will be ample working time dedicated to collaborative projects, including formalization 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.
Specific projects will be determined closer to the start of the workshop. Feel free to contact us if you have suggestions!
We will be using the Lean and LMFDB Zulip servers to organize ourselves before and during the workshop. If you are not yet a member, either of the organizers can send you an invitation.
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 formalization. Due to limited space, registration will be mandatory through our application form by Wednesday, September 30, 2026, with some funding for travel and accommodation for early career researchers. While no background in Lean or formalization will be necessary for participation, it will be immensely helpful to have some interest in the formalization of number theory or large-scale databases in Lean.
David Roe and Andrew Sutherland.
Please contact roed@mit.edu or drew@math.mit.edu with any questions.
accessibility