University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Certifying Synthetic Mathematics in Lean

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Certifying Synthetic Mathematics in Lean

Download to your calendar using vCal

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:

Note that ex-directory lists are not shown.

Other lists

nlip seminar Pavilion room. Hughes Hall College Stokes Society, Pembroke College

Other talks

Group Presentation 1 Early cancer clinical trials Filial Lines: Art Spiegelman, Alison Bechdel, and Comics Form Beyond Hubble: Studying the Earliest Galaxies with the James Webb Space Telescope title abstract tba A scientists guide to the art of radiation therapy and Neurosurgery for the oncologist
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity