![[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)
Axel LjungstrΓΆm (University of Nottingham).
Thursday 26 February 2026, 17:00-18:00
MR14 Centre for Mathematical Sciences
Contact: No managers listed
0 upcoming talks View 39 archived talks
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
Combining Two Representations of Matrices for a Formalization of the Perron-Frobenius Theorem
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
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
Cambridge Image Analysis Seminars
Neural Fields for Embedded Variational Problems in Imaging
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
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
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
CCIMI Seminars
Spectral rigidity of the round Earth
CMIH short course: Image Reconstruction in Biomedical Imaging
Image Reconstruction in Biomedical Imaging: Multimodality imaging
β οΈ Note Time and Room Changed
CMIH short course: Image Reconstruction in Biomedical Imaging
Image Reconstruction in Biomedical Imaging: Motion correction in dynamic imaging
β οΈ Note Room Changed
CCIMI Seminars
On the long time stability of travelling wave for the discrete nonlinear Schroedinger equations
CCIMI Seminars
From Infinite to Finite Programs: Explicit Error Bounds with Applications to Approximate Dynamic Programming
Please see above for contact details for this list.