![[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
Formalisation of mathematics with interactive theorem provers
This is a joint seminar series between the Department of Computer Science and Technology and the Faculty of Mathematics, on the fast-growing area of formalisation of mathematics with proof assistants (interactive theorem provers) such as Isabelle and Lean. All levels welcome. Undergraduate students are particularly encouraged to actively participate.
Talk recordings can be found on our YouTube channel.
Contact: HoD Secretary, DPMMS ; Angeliki Koutsoukou-Argyraki ; Mantas Bakšys ; Anand Rao Tadipatri ; Jonas Bayer
2 upcoming talks View 68 archived talks
Why do I write proofs?
Can a computer judge interestingness?
Lawvere Theories in Lean
Structures in dependent type theory
How to prove Fermat's Last Theorem
Towards Autoformalization and Mathematical Reasoning using language models
Roth numbers: Upper, lower bounds, and related constructions
Formalizing the change of variables formula for integrals in mathlib
Formalizing algebraic number theory, recent progress and future challenges
The leanest automata
Explaining mathematics using formalized mathematics
Formalization of diagram chasing as a first-order logic in Coq
Smooth vector bundles in Lean
[CANCELLED] Real Closed Field and Thom Encoding in Isabelle/HOL
Formalising Turán's Graph Theorem in Isabelle/HOL
Some practical problems in formalising mathematics and how to solve them
How Hilbert met Isabelle: Proof Between Generations
Please see above for contact details for this list.