Certifying Synthetic Mathematics in Lean

Add to your list(s) Download to your calendar using vCal

• Wojciech Nawrocki (Carnegie Mellon University)
• Thursday 19 February 2026, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

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.

In this talk we will present SynthLean: a proof assistant that fills this gap by combining reasoning using synthetic theories with reasoning about their models.

SynthLean is part of the HoTTLean project, presented by Steve Awodey in this seminar series a week prior (on February 12th).

=== Online talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1

Meeting ID: 898 5609 1954 Passcode: ITPtalk

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• Martin's interesting talks
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk449

Note that ex-directory lists are not shown.