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

What We Do

Deep Tech Backed by Theoretical Science

We are a deep tech organisation rooted in the rigour of theoretical science. Our interests span quantum computing, formal methods, and the mathematical foundations that underpin next-generation technology. At our core, we invest in mathematical formalisation — building the structured datasets and verification tools in Lean 4 that enable AI systems to reason with library-quality precision, not just surface-level correctness. We partner with frontier research institutions and the Lean/Mathlib community to build training infrastructure for code-verified AI reasoning.

Explore Our Research

Quantum Computing

Exploring the intersection of quantum information science and formal verification — investing in the mathematical infrastructure that quantum technologies will demand.

Formal Methods

Developing formal mathematical datasets in Lean 4 and building verification tools that capture not just correct proofs, but library-quality formalisations.

Research Programs

Talk series with Nobel laureates and Fields medalists, winter schools in theoretical physics, and talent pipelines from overlooked regions into frontier research.

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