data David = Research | Activities | Events | Talks | Miscellaneous | Lean-LMFDB

This page was generated by Haskell on 25.12.25 with theme inspired by GHCi.

*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