![[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
DPMMS Pure Maths study groups
study groups in pure maths
Contact: HoD Secretary, DPMMS
2 upcoming talks View 98 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
The Serre finiteness theorem in Cubical Agda
Formalisation of mathematics with interactive theorem provers
Certifying Synthetic Mathematics in Lean
Formalisation of mathematics with interactive theorem provers
HoTTLean: Semantics of HoTT in Lean
Formalisation of mathematics with interactive theorem provers
Aristotle, an AI theorem prover using Lean
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
Integrating Formal and Informal Reasoning
Formalisation of mathematics with interactive theorem provers
Combining Two Representations of Matrices for a Formalization of the Perron-Frobenius Theorem
Formalisation of mathematics with interactive theorem provers
Human oriented tools for theorem proving in Lean
Formalisation of mathematics with interactive theorem provers
Lambda-Superposition for Successful Hammering
Formalisation of mathematics with interactive theorem provers
A Lean Tactic to Automatically Generalize Proofs
Formalisation of mathematics with interactive theorem provers
Using interactive theorem provers in physics
Formalisation of mathematics with interactive theorem provers
The Road to Formalising 8-Dimensional Sphere Packing in Lean
Formalisation of mathematics with interactive theorem provers
Formalising the Multigraded Proj Construction in Lean 4
Formalisation of mathematics with interactive theorem provers
Universal Diophantine Equations in Isabelle
Formalisation of mathematics with interactive theorem provers
Completeness Theorems for Variations of Higher-Order Logic
โ ๏ธ CANCELLED
Formalisation of mathematics with interactive theorem provers
Algebraic Geometry in Mathlib
Formalisation of mathematics with interactive theorem provers
Formalizing Fermat: an update
Formalisation of mathematics with interactive theorem provers
Verified Unsolvability of Temporal Planning
Formalisation of mathematics with interactive theorem provers
Formal verification of the 5th Busy Beaver value
Formalisation of mathematics with interactive theorem provers
Why do I write proofs?
โ ๏ธ NOTE UNUSUAL DAY
Formalisation of mathematics with interactive theorem provers
Formalising Brauer Group and Group Cohomology in Lean4
Formalisation of mathematics with interactive theorem provers
Algebraising foundations of elliptic curves
Formalisation of mathematics with interactive theorem provers
Formalisation of Combinatorial Optimisation in Isabelle/HOL: Network Flows
Formalisation of mathematics with interactive theorem provers
Prospects for formalizing the theory of weak infinite-dimensional categories
Formalisation of mathematics with interactive theorem provers
Decision Procedures for Bitvector Reasoning in Lean
Formalisation of mathematics with interactive theorem provers
How to teach Fourier analysis to a large library of formalised mathematics
Formalisation of mathematics with interactive theorem provers
Automatic Verification of BitVector Identities in SSA-Based Compiler IRs
Formalisation of mathematics with interactive theorem provers
Computer Algebra and the Formalisation of New Mathematics
Formalisation of mathematics with interactive theorem provers
Formalizing the divided power envelope in Lean
Formalisation of mathematics with interactive theorem provers
A tour in (formalised) type theory
Formalisation of mathematics with interactive theorem provers
Equational theories project: metatheorems and how to formalise them
Formalisation of mathematics with interactive theorem provers
New Foundations: the story of a large formalisation project
Formalisation of mathematics with interactive theorem provers
Computer environments for math problem solving
Formalisation of mathematics with interactive theorem provers
Reasoning with Kan fillings about Morse reductions
Formalisation of mathematics with interactive theorem provers
Alpha-Beta Pruning Explored, Extended and Verified
Formalisation of mathematics with interactive theorem provers
Little theories for big formal proofs
Formalisation of mathematics with interactive theorem provers
Teaching using a proof assistant and controlled natural language
Formalisation of mathematics with interactive theorem provers
Scientific Computing in Lean
Formalisation of mathematics with interactive theorem provers
Condensed Type Theory
Formalisation of mathematics with interactive theorem provers
Can a computer judge interestingness?
โ ๏ธ (NOTE UNUSUAL DAY/TIME)
Formalisation of mathematics with interactive theorem provers
Formalising Theory of Combinatorial Optimisation
โ ๏ธ Online
Formalisation of mathematics with interactive theorem provers
Lawvere Theories in Lean
โ ๏ธ Online
Formalisation of mathematics with interactive theorem provers
Formalising (part of) the Diagonal Ramsey Paper
Formalisation of mathematics with interactive theorem provers
The Mandelbrot set is connected (and other Lean explorations)
Formalisation of mathematics with interactive theorem provers
Experiences with Isabelle/HOL: Formalising Real Algebraic Geometry
Formalisation of mathematics with interactive theorem provers
Structures in dependent type theory
โ ๏ธ Online
Formalisation of mathematics with interactive theorem provers
How to prove Fermat's Last Theorem
โ ๏ธ Online
Formalisation of mathematics with interactive theorem provers
Comparative Formalisation of Kneser's theorem in Isabelle/HOL and Lean
Formalisation of mathematics with interactive theorem provers
Towards Autoformalization and Mathematical Reasoning using language models
โ ๏ธ Note unusual time
Formalisation of mathematics with interactive theorem provers
Roth numbers: Upper, lower bounds, and related constructions
โ ๏ธ Note: different room, MR20 this time
Formalisation of mathematics with interactive theorem provers
Formalizing the change of variables formula for integrals in mathlib
โ ๏ธ Hybrid talk (please see abstract for link) Note: different room, MR20 this time
Formalisation of mathematics with interactive theorem provers
Formalizing algebraic number theory, recent progress and future challenges
โ ๏ธ Note: different room, MR20 this time
Formalisation of mathematics with interactive theorem provers
The leanest automata
โ ๏ธ Hybrid talk (please see abstract for link) Note: different room, MR20 this time
Formalisation of mathematics with interactive theorem provers
Formalising Erdลs and Larson: Ordinal Partition Theory
Formalisation of mathematics with interactive theorem provers
Explaining mathematics using formalized mathematics
โ ๏ธ Hybrid talk (please see abstract for link)
Formalisation of mathematics with interactive theorem provers
Formalization of diagram chasing as a first-order logic in Coq
โ ๏ธ Hybrid talk (please see abstract for link)
Formalisation of mathematics with interactive theorem provers
Smooth vector bundles in Lean
โ ๏ธ Hybrid talk (please see abstract for link)
Formalisation of mathematics with interactive theorem provers
Formalising modular forms, Eisenstein series and the statement of the modularity conjecture in Lean
Formalisation of mathematics with interactive theorem provers
The Locale-Centric Approach for Formalising Mathematical Hierarchies
Formalisation of mathematics with interactive theorem provers
[CANCELLED] Real Closed Field and Thom Encoding in Isabelle/HOL
โ ๏ธ [CANCELLED, please check back for rescheduling]
Formalisation of mathematics with interactive theorem provers
Formalising Turรกn's Graph Theorem in Isabelle/HOL
โ ๏ธ Hybrid talk (please see abstract for link)
Formalisation of mathematics with interactive theorem provers
Formalisation of the BalogโSzemerรฉdiโGowers Theorem in Isabelle/HOL
Formalisation of mathematics with interactive theorem provers
From benchmark-centric to human-centric: deep learning methods in the formalisation of mathematics
Formalisation of mathematics with interactive theorem provers
Some practical problems in formalising mathematics and how to solve them
โ ๏ธ Hybrid talk (please see abstract for link)
Formalisation of mathematics with interactive theorem provers
The Liquid Tensor Experiment
Formalisation of mathematics with interactive theorem provers
How Hilbert met Isabelle: Proof Between Generations
โ ๏ธ Hybrid talk (please see abstract for link)
Formalisation of mathematics with interactive theorem provers
Formalised Mathematics: Obstacles and Achievements
Motivic stable homotopy theory study group
An Unstable Representability Criterion
Motivic stable homotopy theory study group
Examples of motivic spectra
Motivic stable homotopy theory study group
Stable homotopy theory over general base schemes
Motivic stable homotopy theory study group
Symmetric spectra and motivic symmetric spectra
Motivic stable homotopy theory study group
Stable (infinity-1)-categories
Motivic stable homotopy theory study group
The Thom isomorphism
Motivic stable homotopy theory study group
The Nisnevich topology and the Thom isomorphism
Motivic stable homotopy theory study group
The idea of motivic stable homotopy theory
Number Theory Study Group: P-adic Analysis
Introduction to Lubin-Tate theory
Number Theory Study Group: P-adic Analysis
Locally analytic functions and distributions on Z_p
โ ๏ธ Vladimir to make cake
Number Theory Study Group: P-adic Analysis
Continuous functions and measures on Z_p
โ ๏ธ Sarah to make cake
Number Theory Study Group: P-adic Analysis
Functions defined by power series
โ ๏ธ Tim to make cake
Number Theory Study Group: Langlands correspondence
Functoriality
Number Theory Study Group: Langlands correspondence
L-groups
Number Theory Study Group: Langlands correspondence
Global Langlands correspondence
Number Theory Study Group: Langlands correspondence
Local Langlands Correspondence
Number Theory Study Group: Langlands correspondence
Title to be confirmed
Number Theory Study Group: Langlands correspondence
Automorphic forms
Number Theory Study Group: Langlands correspondence
Algebraic groups
Number Theory Study Group: Langlands correspondence
Introduction and layout of the talks
Study Group on a Langlands Correspondence for Loop Groups
Constructing the Local Langlands Correspondence
Study Group on a Langlands Correspondence for Loop Groups
The center for an arbitrary Kac-Moody algebra
Study Group on a Langlands Correspondence for Loop Groups
Opers
Study Group on a Langlands Correspondence for Loop Groups
The centre of the vertex algebra attached to the central extension of sl_2((t))
Study Group on a Langlands Correspondence for Loop Groups
Lie algebras associated to Vertex algebras and the centre of a Vertex algebra
Study Group on a Langlands Correspondence for Loop Groups
Vertex Algebras II
Study Group on a Langlands Correspondence for Loop Groups
Vertex Algebras I
Study Group on a Langlands Correspondence for Loop Groups
Introductory remarks on the Local Geometric Langlands Correspondence
Please see above for contact details for this list.