A Certifying Proof Assistant for Synthetic Mathematics in LeanCPP 2026 with S. Awodey, M. Carneiro, J. Hua, W. Nawrocki, Shuge Rong , Yiming Xu \ Previous Next