| CARVIEW |
Select Language
HTTP/2 301
server: GitHub.com
content-type: text/html
location: https://multramate.github.io/lean-lmfdb/
access-control-allow-origin: *
strict-transport-security: max-age=31556952
expires: Tue, 30 Dec 2025 11:40:25 GMT
cache-control: max-age=600
x-proxy-cache: MISS
x-github-request-id: A2B6:3946E9:9F60F0:B310BB:6953B7D0
accept-ranges: bytes
age: 0
date: Tue, 30 Dec 2025 11:30:25 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210058-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1767094225.353530,VS0,VE209
vary: Accept-Encoding
x-fastly-request-id: 7a97fb5c524fb2ab5a6854791e87fccf563e9dff
content-length: 162
HTTP/2 200
server: GitHub.com
content-type: text/html; charset=utf-8
last-modified: Thu, 25 Dec 2025 22:06:57 GMT
access-control-allow-origin: *
strict-transport-security: max-age=31556952
etag: W/"694db581-1be1"
expires: Tue, 30 Dec 2025 11:40:25 GMT
cache-control: max-age=600
content-encoding: gzip
x-proxy-cache: MISS
x-github-request-id: 1A18:3946E9:9F60F4:B310BE:6953B7CE
accept-ranges: bytes
age: 0
date: Tue, 30 Dec 2025 11:30:25 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210058-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1767094226.576000,VS0,VE241
vary: Accept-Encoding
x-fastly-request-id: 1c80b3b3da0b3e63db2f751f82b221cb1e7728e1
content-length: 2206
Bridging Lean and the LMFDB
Bridging 
and the 
and the
*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 | |||||