Formalizing Noncommutative Geometry: Proof assistants, knowledge graphs and AI in research

by Christoph Stephan

Wednesday 18 Feb 2026, 16:00 → 17:00 Europe/Rome

0M04

I will give a short introduction to Lean 4 - a proof assistant - and provide an overview of dependent type theory, which underlies its verification capabilities. I will then present project to formalise noncommutative geometry (NCG) in Lean 4 where the long-term goal is the formalization of Connes’ Reconstruction Theorem. While our project is still in its early stages, the Lean community has already laid some of the necessary foundations. 
Lean allows mathematical work to be divided into small, verifiable components, making collaborative research more efficient. To support this process, we are developing tools that assist with proof translation and organization of formalized results. AI is one component of these tools, helping to automate and streamline certain tasks.