A Certifying Proof Assistant for Synthetic Mathematics in Lean

CPP 2026

with S. Awodey, M. Carneiro, J. Hua, W. Nawrocki, Shuge Rong , Yiming Xu \