Formalisation of mathematics with interactive theorem provers 


2023-01-19 17:00: Formalised Mathematics: Obstacles and Achievements (Professor Lawrence C. Paulson FRS (University of Cambridge))

2023-01-26 17:00: How Hilbert met Isabelle: Proof Between Generations (Marco David (École Normale Supérieure de Paris))

2023-02-02 17:00: The Liquid Tensor Experiment (Professor Kevin Buzzard (Imperial College London))

2023-02-09 17:00: Some practical problems in formalising mathematics and how to solve them (Dr Manuel Eberl (University of Innsbruck))

2023-02-16 17:00: From benchmark-centric to human-centric: deep learning methods in the formalisation of mathematics (Albert Qiaochu Jiang (University of Cambridge))

2023-02-23 17:00: Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL (Mantas Bakšys (University of Cambridge))

2023-03-02 17:00: Formalising Turán's Graph Theorem in Isabelle/HOL (Nils Lauermann (INRIA))

2023-03-09 17:00: [CANCELLED] Real Closed Field and Thom Encoding in Isabelle/HOL   (Dr Wenda Li (University of Cambridge), Artem Khovanov (University of Cambridge) and Michael Nedzelsky (Diffblue Ltd))

2023-03-16 17:00: The Locale-Centric Approach for Formalising Mathematical Hierarchies (Chelsea Edmonds (University of Cambridge))

2023-04-27 17:00: Formalising modular forms, Eisenstein series and the statement of the modularity conjecture in Lean (Dr Chris Birkbeck (University of East Anglia))

2023-05-04 17:00: Smooth vector bundles in Lean (Professor Heather Macbeth (Fordham University))

2023-05-11 17:00: Formalization of diagram chasing as a first-order logic in Coq (Dr Matthieu Piquerez (INRIA, Université de Nantes))

2023-05-18 17:00: Explaining mathematics using formalized mathematics (Professor Patrick Massot (Université Paris-Saclay))

2023-05-25 17:00: Formalising Erdős and Larson: Ordinal Partition Theory (Professor Lawrence C. Paulson FRS (University of Cambridge))

2023-06-01 17:00: The leanest automata (Professor Bjørn Kjos-Hanssen (University of Hawaii at Manoa))

2023-06-08 17:00: Formalizing algebraic number theory, recent progress and future challenges (Dr Alex J. Best (King's College London))

2023-06-15 17:00: Formalizing the change of variables formula for integrals in mathlib (Professor Sébastien Gouëzel (Université de Rennes))

2023-06-22 17:00: Roth numbers: Upper, lower bounds, and related constructions (Yaël Dillies (University of Cambridge))

2024-01-17 13:00: Towards Autoformalization and Mathematical Reasoning using language models (Professor Siddhartha Gadgil (Indian Institute of Science))

2024-02-01 17:00: Comparative Formalisation of Kneser's theorem in Isabelle/HOL and Lean (Mantas Bakšys and Yaël Dillies (University of Cambridge))

2024-02-08 17:00: How to prove Fermat's Last Theorem (Professor Kevin Buzzard (Imperial College London))

2024-02-15 17:00: Structures in dependent type theory (Professor Jeremy Avigad (Carnegie Mellon University))

2024-02-22 17:00: Experiences with Isabelle/HOL: Formalising Real Algebraic Geometry (Artie Khovanov (University of Cambridge), Michael Nedzelsky (Diffblue Ltd) and Dr Wenda Li (University of Edinburgh))

2024-02-29 17:00: The Mandelbrot set is connected (and other Lean explorations) (Dr Geoffrey Irving (previously Google DeepMind, soon the UK AI Safety Institute))

2024-03-07 17:00: Formalising (part of) the Diagonal Ramsey Paper (Professor Lawrence Paulson (University of Cambridge))

2024-03-14 17:00: Lawvere Theories in Lean (Professor Adam Topaz (University of Alberta))

2024-04-25 17:00: Formalising Theory of Combinatorial Optimisation (Dr Mohammad Abdulaziz (King's College London))

2024-04-29 14:00: Can a computer judge interestingness? (Professor Michael Douglas (Center of Mathematical Sciences and Applications, Harvard University))

2024-05-02 17:00: Condensed Type Theory (Dr Johan Commelin (Utrecht University))

2024-05-09 17:00: Scientific Computing in Lean (Tomas Skrivan (Carnegie Mellon University))

2024-05-16 17:00: Teaching using a proof assistant and controlled natural language (Professor Patrick Massot (Université Paris-Saclay and Carnegie Mellon University))

2024-05-23 17:00: Little theories for big formal proofs (Professor Georges Gonthier (Inria))

2024-06-13 17:00: Alpha-Beta Pruning Explored, Extended and Verified (Professor Tobias Nipkow (Technische Universität München))

2024-10-10 17:00: Reasoning with Kan fillings about Morse reductions (Maximilian Doré (University of Oxford))

2024-10-17 17:00: Computer environments for math problem solving (Mirek Olšák (University of Cambridge))

2024-10-24 17:00: New Foundations: the story of a large formalisation project (Sky Wilshaw (University of Nottingham))

2024-10-31 17:00: Equational theories project: metatheorems and how to formalise them (Hernán Ibarra Mejia, THG and Anand Rao Tadipatri, University of Cambridge)

2024-11-07 17:00: A tour in (formalised) type theory (Meven Lennon-Bertrand (University of Cambridge))

2024-11-14 17:00: Formalizing the divided power envelope in Lean (María Inés de Frutos-Fernández (University of Bonn))

2024-11-21 17:00: Computer Algebra and the Formalisation of New Mathematics (Lawrence Paulson (University of Cambridge))

2024-11-28 17:00: Automatic Verification of BitVector Identities in SSA-Based Compiler IRs (Tobias Grosser (University of Cambridge))

2024-12-05 17:00: How to teach Fourier analysis to a large library of formalised mathematics (Yaël Dillies (Stockholm Universitet))

2025-01-23 17:00: Decision Procedures for Bitvector Reasoning in Lean (Siddharth Bhat (University of Cambridge))

2025-01-30 17:00: Prospects for formalizing the theory of weak infinite-dimensional categories (Emily Riehl (Johns Hopkins University))

2025-02-06 17:00: Formalisation of Combinatorial Optimisation in Isabelle/HOL: Network Flows (Thomas Ammer (King's College London))

2025-02-13 17:00: Algebraising foundations of elliptic curves (David Angdinata (University College London))

2025-02-20 17:00: Formalising Brauer Group and Group Cohomology in Lean4 (Jujian Zhang (Imperial College London))

2025-03-12 17:00: Why do I write proofs? (Francisco Ferreira Ruiz (Royal Holloway, University of London))

2025-03-13 17:00: Formal verification of the 5th Busy Beaver value (Tristan Stérin (Maynooth University, Ireland) and Maja Kądziołka)

2025-03-20 17:00: Verified Unsolvability of Temporal Planning (David Wang (King's College London))

2025-05-01 17:00: Formalizing Fermat: an update (Kevin Buzzard (Imperial College London))

2025-05-08 17:00: Algebraic Geometry in Mathlib (Andrew Yang (Imperial College, London))

2025-05-22 17:00: Completeness Theorems for Variations of Higher-Order Logic (Andrei Popescu (University of Sheffield))

2025-05-29 17:00: Universal Diophantine Equations in Isabelle (Jonas Bayer (University of Cambridge))

2025-06-19 17:00: Formalising the Multigraded Proj Construction in Lean 4 (Jujian Zhang (Imperial College London) and Arnaud Mayeux (The Hebrew University of Jerusalem))

2025-10-09 17:00: The Road to Formalising 8-Dimensional Sphere Packing in Lean (Sidharth Hariharan (Carnegie Mellon University))

2025-10-16 17:00: Using interactive theorem provers in physics (Joseph Tooby-Smith (University of Bath))

2025-10-30 17:00: A Lean Tactic to Automatically Generalize Proofs (Anshula Gandhi (University of Cambridge))

2025-11-06 17:00: Lambda-Superposition for Successful Hammering (Jasmin Blanchette (Ludwig-Maximilians-Universität München))

2025-11-20 17:00: Human oriented tools for theorem proving in Lean (Jovan Gerbsheid (University of Cambridge))

2025-11-27 17:00: Combining Two Representations of Matrices for a Formalization of the Perron-Frobenius Theorem (René Thiemann (University of Innsbruck))

2025-12-04 17:00: Integrating Formal and Informal Reasoning (Chase Norman (Carnegie Mellon University))

2026-01-22 17:00: Lean4Less: Translating Lean to Smaller Theories via an Extensional-to-Intensional Translation (Rishikesh Vaishnav (ENS Paris-Saclay))

2026-01-29 17:00: Aristotle, an AI theorem prover using Lean (Alex J Best (Harmonic))

2026-02-12 17:00: HoTTLean: Semantics of HoTT in Lean (Steve Awodey (Royal Society Wolfson Visiting Fellow at Cambridge CST))

2026-02-19 17:00: Certifying Synthetic Mathematics in Lean (Wojciech Nawrocki (Carnegie Mellon University))

2026-02-26 17:00: The Serre finiteness theorem in Cubical Agda (Axel Ljungström (University of Nottingham))

2026-03-12 17:00: Faithful Logic Embeddings in HOL:  Deep and Shallow, Propositional and Quantified (Christoph Benzmüller (Otto-Friedrich-Universität Bamberg and Freie Universität Berlin))

2026-04-30 17:00: Title to be confirmed (Floris van Doorn (University of Bonn))

2026-05-28 17:00: Title to be confirmed (Thomas Powell (University of Bath))