Research &
Infrastructure
Formal Verification · AI Theorem Proving · Lean 4 Datasets
Core Research
Formal Mathematics & AI Theorem Proving
Mathematical formalisation faces a human capital crisis. Fewer than a few hundred people worldwide can formalise graduate-level mathematics in Lean 4 at library quality. The bottleneck is not tooling or compute — it is people who produce formalisations that are maintainable, correctly generalised, and integrable into mathematical libraries.
Launching 2026 · Bonn + Remote · In Partnership with World Scientific
Lean 4 Formalization Workshop
An intensive 10-week training programme that takes mathematicians from zero Lean experience to certified library-quality formalisers who have completed a real Mathlib PR review cycle. The programme addresses three integrated outputs:
People
Training talented mathematicians to produce Mathlib-quality formalisations — directly feeding the upstream pipeline that the broader Lean ecosystem needs. Each cohort trains ~20 participants from Bonn and internationally.
Data
Every formalisation generates a structured process trace: the complete record of attempts, errors, corrections, AI interactions, and quality-improvement decisions. A novel data type — no "PRM800K for formal proofs" currently exists.
Tools
A quality-aware formalisation assistant trained on our process trace corpus. Unlike existing autoformalisers that optimise for correctness alone, this system integrates library-quality evaluation into the generation loop.
Scientific Advisor: Prof. Yang-Hui He (London Institute for Mathematical Sciences). Programme Director: Rajarshi Maiti (University of Bonn). AI & ML Lead: Dr Edward Hirst (University of London / UNICAMP).
ApplyWhy This Matters
AI-assisted formalisation tools increasingly generate Lean code that compiles but does not meet library standards. The Mathlib community faces a rising tide of AI-generated submissions that require more effort to review than to rewrite — while the review pipeline has over 2,000 open pull requests and fewer than 60 active reviewers.
BMUCO addresses both the talent bottleneck and the quality gap. Our training produces the people; our process traces produce the data; and our tools integrate quality evaluation into the generation loop. All outputs are designed to be complementary to existing efforts in the Lean/Mathlib ecosystem.
Student Research
Research Supervision Program
Under Dr Edward Hirst (PhD in Math+ML at the University of London): 3-month Summer Research Assistant Program. BMUCO Summer Fellow Devashish delved into a fascinating machine learning project focused on dessins.
Past Programs
Winter School in Quantum Physics
Date and Time: 4th - 11th January 2021
This Winter school was delivered online via Zoom, targeting Undergraduate students interested in pursuing a research career in mathematics and physics. Lectures covered the background needed for quantum field theory, including classical field theory, special relativity, and quantum mechanics, eventually leading to Quantum Field Theory.
Topics Covered
- Classical Field theory and Special relativity: Elijah Cavan, University of Waterloo (4th & 6th)
- Quantum Mechanics: Prof Gleb Gribarkin, Queen's University Belfast (8th)
- Quantum Field Theory: Prof Neil Lambert, King's College London (11th)
Topic Description
Quantum Field Theory (QFT) is the mathematical and conceptual framework for contemporary elementary particle physics. It is also a framework used in other areas of theoretical physics, such as condensed matter physics and statistical mechanics.
Quantum mechanics is a fundamental theory in physics that provides a description of the physical properties of nature at the scale of atoms and subatomic particles. It is the foundation of all quantum physics including quantum chemistry, quantum field theory, quantum technology, and quantum information science.
Classical field theory predicts how one or more physical fields interact with matter through field equations. The term is commonly reserved for describing those physical theories that describe electromagnetism and gravitation.
Special relativity plays an important role in the modern theory of classical electromagnetism, providing formulas for how electromagnetic objects are altered under a Lorentz transformation and explaining how to transform Maxwell's equations.
Climate Science & Policy
Science-Driven Climate Action
BMUCO-affiliated youth delegates have represented young voices at UN climate conferences including SB60 and SB62, bridging rigorous science with climate justice. Our Climate Dialogues bring together scientists, policymakers, and youth from affected regions in pre-COP engagements — grounding climate action in evidence.