This is a workshop to bridge the Lean theorem prover and the L-functions and modular forms database. It will feature tutorials to navigate the number theory interface in mathlib as well as research talks in relevant areas. There will also be ample working time dedicated to projects, including formalisation of definitions in the LMFDB as in the blueprint. Registration will be mandatory through our application form by Saturday, 28 February 2026, with some funding for travel and accommodation. Please visit the website for more details.