Domain Specific

Documentation for Mathlib

The project aims to bridge the gap for mathematicians interested in formalization by creating accessible, domain-specific guides to theorem proving in Lean. Targeting mathematicians at the graduate level and above, this work focuses on areas such as Algebraic Number Theory and Graph Theory, where existing Mathlib APIs are well-developed but challenging for non-experts. By providing overviews, examples, and exercises modeled after successful resources, the project seeks to enhance understanding and participation in formalization, ultimately expanding the high-quality Lean code available for AI model training.

The Project

The Team

John Talbot was GCHQ Research Fellow at the University of Oxford and then held a Royal Society University Research Fellowship at UCL. He is currently Associate Professor of Pure Mathematics at UCL, working in extremal and probabilistic combinatorics. He has recently developed an interest in proof formalization in Lean.

Richard M. Hill has held research positions in Goettingen and the Max-Planck Institute (Bonn) and is now Professor of Pure Mathematics at UCL.