Formal
Mathematics
Meets AI

We develop formal mathematical datasets in Lean 4 and build AI theorem proving infrastructure — partnering with frontier research institutions to advance the science of automated reasoning.

Our Research Get in Touch

Hausdorff Centre for MathematicsLondon Institute for Mathematical SciencesEPSRC National Edge AI HubQueen's University BelfastHausdorff Centre for MathematicsLondon Institute for Mathematical SciencesEPSRC National Edge AI HubQueen's University BelfastHausdorff Centre for MathematicsLondon Institute for Mathematical SciencesEPSRC National Edge AI HubQueen's University BelfastHausdorff Centre for MathematicsLondon Institute for Mathematical SciencesEPSRC National Edge AI HubQueen's University Belfast

How It Connects

Three pillars, one infrastructure

Formalisation →

Lean 4 · Mathlib · Process Traces

Theoretical Science →

Physics · Pure Mathematics · Geometry

Talk series with Nobel Laureates and Fields Medalists. Winter schools in theoretical physics. Research programmes bridging pure mathematics and frontier science — open to anyone with drive, regardless of institution.

AI Theorem Proving →

Automated Reasoning · Verification · ML

What We Do

Formal Mathematics & AI

We build the datasets and tools that mathematical AI needs. Our work centres on formal mathematical datasets in Lean 4 for AI theorem proving — structured process traces that capture not just correct proofs, but library-quality formalisations. We partner with frontier AI organisations and the Lean/Mathlib community to build training infrastructure for automated reasoning.

Explore Our Research

Research Programs

Talk series with Nobel laureates and Fields medalists, winter schools in theoretical physics, intensive research training, and one-on-one mentorships — building talent pipelines from overlooked regions into frontier research.

Science-Driven Climate Policy

Youth delegations at UN climate convenings including SB60 and SB62, bridging rigorous science with climate justice — grounding policy in evidence.

Launching 2026 · Bonn + Remote

Lean 4
Formalization
Workshop

An intensive training programme that takes mathematicians from zero Lean experience to library-quality formalisers — producing the structured process trace datasets that power AI theorem proving. In partnership with World Scientific.

People. Training the next generation of formalisation researchers who can produce Mathlib-quality contributions.

Data. Every formalisation generates a structured process trace — the training signal for mathematical AI.

Tools. Building quality-aware formalisation infrastructure for the Lean/Mathlib ecosystem.

Learn More Apply

Scientific Community