Formalisation of mathematics with interactive theorem provers

Completeness Theorems for Variations of Higher-Order Logic

CANCELLED

Andrei Popescu (University of Sheffield).

Online; live-streamed at MR14 Centre for Mathematical Sciences.

Thursday 22 May 2025, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Algebraic Geometry in Mathlib

Andrew Yang (Imperial College, London).

MR14 Centre for Mathematical Sciences.

Thursday 08 May 2025, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Formalizing Fermat: an update

Kevin Buzzard (Imperial College London).

MR14 Centre for Mathematical Sciences.

Thursday 01 May 2025, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Verified Unsolvability of Temporal Planning

David Wang (King's College London).

MR14 Centre for Mathematical Sciences.

Thursday 20 March 2025, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Formal verification of the 5th Busy Beaver value

Tristan Stérin (Maynooth University, Ireland) and Maja Kądziołka.

MR14 Centre for Mathematical Sciences.

Thursday 13 March 2025, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Why do I write proofs?

NOTE UNUSUAL DAY

Francisco Ferreira Ruiz (Royal Holloway, University of London).

MR14 Centre for Mathematical Sciences.

Wednesday 12 March 2025, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Formalising Brauer Group and Group Cohomology in Lean4

Jujian Zhang (Imperial College London).

MR14 Centre for Mathematical Sciences.

Thursday 20 February 2025, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Algebraising foundations of elliptic curves

David Angdinata (University College London).

MR14 Centre for Mathematical Sciences.

Thursday 13 February 2025, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Formalisation of Combinatorial Optimisation in Isabelle/HOL: Network Flows

Thomas Ammer (King's College London).

MR14 Centre for Mathematical Sciences.

Thursday 06 February 2025, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Prospects for formalizing the theory of weak infinite-dimensional categories

Emily Riehl (Johns Hopkins University).

MR14 Centre for Mathematical Sciences.

Thursday 30 January 2025, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Decision Procedures for Bitvector Reasoning in Lean

Siddharth Bhat (University of Cambridge).

MR14 Centre for Mathematical Sciences.

Thursday 23 January 2025, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

How to teach Fourier analysis to a large library of formalised mathematics

Yaël Dillies (Stockholm Universitet).

MR14 Centre for Mathematical Sciences.

Thursday 05 December 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Automatic Verification of BitVector Identities in SSA-Based Compiler IRs

Tobias Grosser (University of Cambridge).

MR14 Centre for Mathematical Sciences.

Thursday 28 November 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Computer Algebra and the Formalisation of New Mathematics

Lawrence Paulson (University of Cambridge).

MR14 Centre for Mathematical Sciences.

Thursday 21 November 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Formalizing the divided power envelope in Lean

María Inés de Frutos-Fernández (University of Bonn).

MR14 Centre for Mathematical Sciences.

Thursday 14 November 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

A tour in (formalised) type theory

Meven Lennon-Bertrand (University of Cambridge).

MR14 Centre for Mathematical Sciences.

Thursday 07 November 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Equational theories project: metatheorems and how to formalise them

Hernán Ibarra Mejia, THG and Anand Rao Tadipatri, University of Cambridge.

MR14 Centre for Mathematical Sciences.

Thursday 31 October 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

New Foundations: the story of a large formalisation project

Sky Wilshaw (University of Nottingham).

MR14 Centre for Mathematical Sciences.

Thursday 24 October 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Computer environments for math problem solving

Mirek Olšák (University of Cambridge).

MR14 Centre for Mathematical Sciences.

Thursday 17 October 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Reasoning with Kan fillings about Morse reductions

Maximilian Doré (University of Oxford).

MR14 Centre for Mathematical Sciences.

Thursday 10 October 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Alpha-Beta Pruning Explored, Extended and Verified

Professor Tobias Nipkow (Technische Universität München).

Live-streamed at MR14 Centre for Mathematical Sciences.

Thursday 13 June 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Little theories for big formal proofs

Professor Georges Gonthier (Inria).

Live-streamed at MR14 Centre for Mathematical Sciences.

Thursday 23 May 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Teaching using a proof assistant and controlled natural language

Professor Patrick Massot (Université Paris-Saclay and Carnegie Mellon University).

Live-streamed at MR14 Centre for Mathematical Sciences.

Thursday 16 May 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Scientific Computing in Lean

Tomas Skrivan (Carnegie Mellon University).

Live-streamed at MR14 Centre for Mathematical Sciences.

Thursday 09 May 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Condensed Type Theory

Dr Johan Commelin (Utrecht University).

Live-streamed at MR14 Centre for Mathematical Sciences.

Thursday 02 May 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Can a computer judge interestingness?

(NOTE UNUSUAL DAY/TIME)

Professor Michael Douglas (Center of Mathematical Sciences and Applications, Harvard University).

MR15 Centre for Mathematical Sciences.

Monday 29 April 2024, 14:00-15:00

Formalisation of mathematics with interactive theorem provers

Formalising Theory of Combinatorial Optimisation

Online

Dr Mohammad Abdulaziz (King's College London).

Live-streamed at MR14 Centre for Mathematical Sciences.

Thursday 25 April 2024, 17:00-18:00

DPMMS Departmental Colloquia

When is a mathematical object well behaved?

Julia Wolf (Cambridge).

CMS MR2.

Thursday 25 April 2024, 16:00-17:00

Formalisation of mathematics with interactive theorem provers

Lawvere Theories in Lean

Online

Professor Adam Topaz (University of Alberta).

Live-streamed at MR14 Centre for Mathematical Sciences.

Thursday 14 March 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Formalising (part of) the Diagonal Ramsey Paper

Professor Lawrence Paulson (University of Cambridge).

MR14 Centre for Mathematical Sciences.

Thursday 07 March 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

The Mandelbrot set is connected (and other Lean explorations)

Dr Geoffrey Irving (previously Google DeepMind, soon the UK AI Safety Institute).

MR14 Centre for Mathematical Sciences.

Thursday 29 February 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Experiences with Isabelle/HOL: Formalising Real Algebraic Geometry

Artie Khovanov (University of Cambridge), Michael Nedzelsky (Diffblue Ltd) and Dr Wenda Li (University of Edinburgh).

MR14 Centre for Mathematical Sciences.

Thursday 22 February 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Structures in dependent type theory

Online

Professor Jeremy Avigad (Carnegie Mellon University).

Live-streamed at MR14 Centre for Mathematical Sciences.

Thursday 15 February 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

How to prove Fermat's Last Theorem

Online

Professor Kevin Buzzard (Imperial College London).

Live-streamed at MR14 Centre for Mathematical Sciences.

Thursday 08 February 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Comparative Formalisation of Kneser's theorem in Isabelle/HOL and Lean

Mantas Bakšys and Yaël Dillies (University of Cambridge).

MR14 Centre for Mathematical Sciences.

Thursday 01 February 2024, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Towards Autoformalization and Mathematical Reasoning using language models

Note unusual time

Professor Siddhartha Gadgil (Indian Institute of Science).

MR14 Centre for Mathematical Sciences.

Wednesday 17 January 2024, 13:00-14:00

Formalisation of mathematics with interactive theorem provers

Roth numbers: Upper, lower bounds, and related constructions

Note: different room, MR20 this time

Yaël Dillies (University of Cambridge).

MR20 Centre for Mathematical Sciences.

Thursday 22 June 2023, 17:00-18:00

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

Professor Sébastien Gouëzel (Université de Rennes).

MR20 Centre for Mathematical Sciences.

Thursday 15 June 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Formalizing algebraic number theory, recent progress and future challenges

Note: different room, MR20 this time

Dr Alex J. Best (King's College London).

MR20 Centre for Mathematical Sciences.

Thursday 08 June 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

The leanest automata

Hybrid talk (please see abstract for link) Note: different room, MR20 this time

Professor Bjørn Kjos-Hanssen (University of Hawaii at Manoa).

MR20 Centre for Mathematical Sciences.

Thursday 01 June 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Formalising Erdős and Larson: Ordinal Partition Theory

Professor Lawrence C. Paulson FRS (University of Cambridge).

Centre for Mathematical Sciences MR12, CMS.

Thursday 25 May 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Explaining mathematics using formalized mathematics

Hybrid talk (please see abstract for link)

Professor Patrick Massot (Université Paris-Saclay).

Centre for Mathematical Sciences MR12, CMS.

Thursday 18 May 2023, 17:00-18:00

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)

Dr Matthieu Piquerez (INRIA, Université de Nantes).

Centre for Mathematical Sciences MR12, CMS.

Thursday 11 May 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Smooth vector bundles in Lean

Hybrid talk (please see abstract for link)

Professor Heather Macbeth (Fordham University).

Centre for Mathematical Sciences MR12, CMS.

Thursday 04 May 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Formalising modular forms, Eisenstein series and the statement of the modularity conjecture in Lean

Dr Chris Birkbeck (University of East Anglia).

Centre for Mathematical Sciences MR12, CMS.

Thursday 27 April 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

The Locale-Centric Approach for Formalising Mathematical Hierarchies

Chelsea Edmonds (University of Cambridge).

Centre for Mathematical Sciences MR12, CMS.

Thursday 16 March 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

[CANCELLED] Real Closed Field and Thom Encoding in Isabelle/HOL

[CANCELLED, please check back for rescheduling]

Dr Wenda Li (University of Cambridge), Artem Khovanov (University of Cambridge) and Michael Nedzelsky (Diffblue Ltd).

Centre for Mathematical Sciences MR12, CMS.

Thursday 09 March 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Formalising Turán's Graph Theorem in Isabelle/HOL

Hybrid talk (please see abstract for link)

Nils Lauermann (INRIA).

Centre for Mathematical Sciences MR12, CMS.

Thursday 02 March 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL

Mantas Bakšys (University of Cambridge).

Centre for Mathematical Sciences MR12, CMS.

Thursday 23 February 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

From benchmark-centric to human-centric: deep learning methods in the formalisation of mathematics

Albert Qiaochu Jiang (University of Cambridge).

Centre for Mathematical Sciences MR12, CMS.

Thursday 16 February 2023, 17:00-18:00

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)

Dr Manuel Eberl (University of Innsbruck).

Centre for Mathematical Sciences MR12, CMS.

Thursday 09 February 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

The Liquid Tensor Experiment

Professor Kevin Buzzard (Imperial College London).

Centre for Mathematical Sciences MR12, CMS.

Thursday 02 February 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

How Hilbert met Isabelle: Proof Between Generations

Hybrid talk (please see abstract for link)

Marco David (École Normale Supérieure de Paris).

Centre for Mathematical Sciences MR12, CMS.

Thursday 26 January 2023, 17:00-18:00

Formalisation of mathematics with interactive theorem provers

Formalised Mathematics: Obstacles and Achievements

Professor Lawrence C. Paulson FRS (University of Cambridge).

Centre for Mathematical Sciences MR12, CMS.

Thursday 19 January 2023, 17:00-18:00

Motivic stable homotopy theory study group

An Unstable Representability Criterion

Marcus Zibrowius ( University of Cambridge).

somewhere in the Centre for Mathematical Sciences.

Friday 26 February 2010, 16:30-18:00

Motivic stable homotopy theory study group

Examples of motivic spectra

Peter Arndt (Göttingen).

Venue to be confirmed.

Tuesday 23 February 2010, 16:30-18:00

Motivic stable homotopy theory study group

Stable homotopy theory over general base schemes

Andreas Holmstrom (University of Cambridge).

MR11, Centre for Mathematical Sciences.

Thursday 18 February 2010, 16:30-18:00

Motivic stable homotopy theory study group

Symmetric spectra and motivic symmetric spectra

Peter Arndt ( Göttingen).

MR5, Centre for Mathematical Sciences.

Tuesday 16 February 2010, 17:00-18:30

Motivic stable homotopy theory study group

Stable (infinity-1)-categories

Alexander Shannon (University of Cambridge).

MR11, Centre for Mathematical Sciences.

Thursday 04 February 2010, 17:00-18:00

Motivic stable homotopy theory study group

The Thom isomorphism

Marcus Zibrowius, University of Cambridge.

MR3, Centre for Mathematical Sciences.

Tuesday 02 February 2010, 17:00-18:00

Motivic stable homotopy theory study group

The Nisnevich topology and the Thom isomorphism

Marcus Zibrowius, University of Cambridge.

MR11, Centre for Mathematical Sciences.

Thursday 28 January 2010, 16:30-18:00

Motivic stable homotopy theory study group

The idea of motivic stable homotopy theory

Peter Arndt, Göttingen.

MR5, Centre for Mathematical Sciences.

Tuesday 19 January 2010, 17:00-18:30

Number Theory Study Group: P-adic Analysis

Introduction to Lubin-Tate theory

Rachel Newton (University of Cambridge).

MR13, CMS.

Thursday 19 November 2009, 14:00-15:00

Number Theory Study Group: P-adic Analysis

The Fourier transform for Z_p

Sarah to make cake

David Loeffler (University of Cambridge).

MR5, CMS.

Thursday 12 November 2009, 14:00-15:00

Number Theory Study Group: P-adic Analysis

Locally analytic functions and distributions on Z_p

Vladimir to make cake

Yunling Kang (Nanjing University).

MR5, CMS.

Thursday 05 November 2009, 14:00-15:00

Number Theory Study Group: P-adic Analysis

Continuous functions and measures on Z_p

Sarah to make cake

Alex Bartel (University of Cambridge).

Discussion Room, Newton Institute.

Thursday 29 October 2009, 14:00-15:00

Number Theory Study Group: P-adic Analysis

Topological vector spaces

Tim to make cake

Chern-Yang Lee (University of Cambridge) and Zhibin Liang (Capital Normal University, Beijing).

Discussion Room, Newton Institute.

Thursday 22 October 2009, 14:00-15:00

Number Theory Study Group: P-adic Analysis

Functions defined by power series

Tim to make cake

Antonio Lei (University of Cambridge).

MR5, CMS.

Thursday 15 October 2009, 14:00-15:00

Number Theory Study Group: Langlands correspondence

Functoriality

Andreas Holmstrom.

MR13.

Wednesday 12 March 2008, 09:00-10:00

Number Theory Study Group: Langlands correspondence

L-groups

Gergely Zabradi.

MR13.

Thursday 06 March 2008, 13:00-14:30

Number Theory Study Group: Langlands correspondence

Global Langlands correspondence

Mahesh Kakde.

MR13.

Thursday 28 February 2008, 13:00-14:30

Number Theory Study Group: Langlands correspondence

Local Langlands Correspondence

Alex Chmelnitzki.

MR13.

Thursday 21 February 2008, 13:00-14:30

Number Theory Study Group: Langlands correspondence

Title to be confirmed

Chern-Yang Lee/Alex Chmelnitzki.

MR13.

Thursday 14 February 2008, 13:00-14:30

Number Theory Study Group: Langlands correspondence

Automorphic forms

Chern-Yang Lee.

MR13.

Thursday 07 February 2008, 13:00-14:30

Number Theory Study Group: Langlands correspondence

Algebraic groups

Ant Lei.

MR13.

Thursday 31 January 2008, 13:00-14:30

Number Theory Study Group: Langlands correspondence

Introduction and layout of the talks

Tobias Berger (DPMMS).

MR13.

Thursday 24 January 2008, 13:00-14:30

Study Group on a Langlands Correspondence for Loop Groups

Constructing the Local Langlands Correspondence

Speaker to be confirmed.

MR 4.

Tuesday 20 November 2007, 16:00-18:00

Study Group on a Langlands Correspondence for Loop Groups

The center for an arbitrary Kac-Moody algebra

Speaker to be confirmed.

MR 4.

Tuesday 13 November 2007, 16:00-18:00

Study Group on a Langlands Correspondence for Loop Groups

Opers

Speaker to be confirmed.

MR 4.

Tuesday 06 November 2007, 16:00-18:00

Study Group on a Langlands Correspondence for Loop Groups

The centre of the vertex algebra attached to the central extension of sl_2((t))

Speaker to be confirmed.

MR 4.

Tuesday 30 October 2007, 16:00-18:00

Study Group on a Langlands Correspondence for Loop Groups

Lie algebras associated to Vertex algebras and the centre of a Vertex algebra

Speaker to be confirmed.

MR 4.

Tuesday 23 October 2007, 16:00-18:00

Study Group on a Langlands Correspondence for Loop Groups

Vertex Algebras II

Mahesh Kakde.

MR 4.

Tuesday 16 October 2007, 16:00-18:00

Study Group on a Langlands Correspondence for Loop Groups

Vertex Algebras I

M. Strauch, DPMMS.

MR 4.

Tuesday 09 October 2007, 16:30-18:00

Study Group on a Langlands Correspondence for Loop Groups

Introductory remarks on the Local Geometric Langlands Correspondence

M. Strauch, DPMMS.

MR 13.

Friday 05 October 2007, 16:00-18:00