[CPP'26] A Certifying Proof Assistant for Synthetic Mathematics in Lean

A Certifying Proof Assistant for Synthetic Mathematics in Lean (Video, CPP 2026) Wojciech Nawrocki, Joseph Hua, Mario Carneiro, Yiming Xu, Spencer Woolfson, Shuge Rong, Sina Hazratpour, Steve Awodey (Carnegie Mellon University, USA; Carnegie Mellon University, USA; Chalmers University of Technology, Sweden; LMU Munich, Germany; Chapman University, USA; Carnegie Mellon University, USA; Stockholm University, Sweden; Carnegie Mellon University, USA) Abstract: \emph{Synthetic} theories such as homotopy type theory axiomatize classical mathematical objects such as spaces up to homotopy. Although theorems in synthetic theories translate to theorems about the axiomatized structures on paper, this fact has not yet been exploited in proof assistants. This makes it challenging to formalize results in classical mathematics using synthetic methods. For example, Cubical Agda supports reasoning about cubical types, but cubical proofs have not been translated to proofs about cubical set models, let alone their topological realizations. To bridge this gap, we present \texttt{SynthLean}: a proof assistant that combines reasoning using synthetic theories with reasoning about their models. \texttt{SynthLean} embeds Martin-Löf type theory as a domain-specific language in Lean, supporting a bidirectional workflow: constructions can be made internally in Martin-Löf type theory as well as externally in a model of the theory. A certifying normalization-by-evaluation typechecker automatically proves that internal definitions have sound interpretations in any model; conversely, semantic entities can be axiomatized in the syntax. Our implementation handles universes, $\Sigma$, $\Pi$, and identity types, as well as arbitrary axiomatized constants. To provide a familiar experience for Lean users, we reuse Lean's tactic language and syntax in the internal mode, and base our formalization of natural model semantics on Mathlib. By taking a generic approach, \texttt{SynthLean} can be used to mechanize various interpretations of internal languages such as the groupoid, cubical, or simplicial models of homotopy type theory in \texttt{HoTTLean}. Article: https://doi.org/10.1145/3779031.3779087 Supplementary archive: https://doi.org/10.5281/zenodo.17798253 (Badges: Artifacts Available) ORCID: https://orcid.org/0000-0002-8839-0618, https://orcid.org/0009-0006-7993-3517, https://orcid.org/0000-0002-0470-5249, https://orcid.org/0009-0002-4006-0983, https://orcid.org/0009-0009-0943-7560, https://orcid.org/0009-0009-6492-5428, https://orcid.org/0000-0002-7921-9149, https://orcid.org/0000-0001-9005-179X Video Tags: type theory, categorical logic, proof assistants, Lean, doi:10.1145/3779031.3779087, doi:10.5281/zenodo.17798253, orcid:0000-0002-8839-0618, orcid:0009-0006-7993-3517, orcid:0000-0002-0470-5249, orcid:0009-0002-4006-0983, orcid:0009-0009-0943-7560, orcid:0009-0009-6492-5428, orcid:0000-0002-7921-9149, orcid:0000-0001-9005-179X, Artifacts Available Presentation at the CPP 2026 conference, Jan 12-13, 2026, https://popl26.sigplan.org/home/CPP-2026/ Sponsored by ACM SIGPLAN.