![[Search]](/static/images/search.gif){kind=small}
![[A-Z Index]](/static/images/az.gif){kind=small}
![[Contact]](/static/images/contact.gif){kind=small}
![[University of Cambridge]](/static/images/identifier2.gif){kind=small}
![[Talks.cam]](/static/images/talkslogosmall.gif)
Christoph Benzmüller (Otto-Friedrich-Universität Bamberg and Freie Universität Berlin).
Thursday 12 March 2026, 17:00-18:00
Online; live-streamed at MR14 Centre for Mathematical Sciences
Contact: No managers listed
1 upcoming talk View 5 archived talks
Formalisation of mathematics with interactive theorem provers
Faithful Logic Embeddings in HOL: Deep and Shallow, Propositional and Quantified
Formalisation of mathematics with interactive theorem provers
Lean4Less: Translating Lean to Smaller Theories via an Extensional-to-Intensional Translation
Formalisation of mathematics with interactive theorem provers
Lambda-Superposition for Successful Hammering
Formalisation of mathematics with interactive theorem provers
Completeness Theorems for Variations of Higher-Order Logic
⚠️ CANCELLED
Formalisation of mathematics with interactive theorem provers
Structures in dependent type theory
⚠️ Online
Please see above for contact details for this list.