University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers

Formalisation of mathematics with interactive theorem provers

Add to your list(s) Send you e-mail reminders Further detail
Subscribe using ical/vcal (Help)

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.

Tell a friend about this list:

If you have a question about this list, please contact: HoD Secretary, DPMMS; Angeliki Koutsoukou-Argyraki; Mantas Bakšys; Anand Rao Tadipatri; Jonas Bayer. If you have a question about a specific talk, click on that talk to find its organiser.

5 upcoming talks and 23 talks in the archive.

Experiences with Isabelle/HOL: Formalising Real Algebraic Geometry

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

HouseMR14 Centre for Mathematical Sciences.

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

Structures in dependent type theory

Online

UserProfessor Jeremy Avigad (Carnegie Mellon University).

HouseLive-streamed at MR14 Centre for Mathematical Sciences.

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

How to prove Fermat's Last Theorem

Online

UserProfessor Kevin Buzzard (Imperial College London).

HouseLive-streamed at MR14 Centre for Mathematical Sciences.

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

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

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

HouseMR14 Centre for Mathematical Sciences.

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

Towards Autoformalization and Mathematical Reasoning using language models

Note unusual time

UserProfessor Siddhartha Gadgil (Indian Institute of Science).

HouseMR14 Centre for Mathematical Sciences.

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

Roth numbers: Upper, lower bounds, and related constructions

Note: different room, MR20 this time

UserYaël Dillies (University of Cambridge).

HouseMR20 Centre for Mathematical Sciences.

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

Formalizing the change of variables formula for integrals in mathlib

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

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

HouseMR20 Centre for Mathematical Sciences.

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

Formalizing algebraic number theory, recent progress and future challenges

Note: different room, MR20 this time

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

HouseMR20 Centre for Mathematical Sciences.

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

The leanest automata

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

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

HouseMR20 Centre for Mathematical Sciences.

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

Formalising Erdős and Larson: Ordinal Partition Theory

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

House Centre for Mathematical Sciences MR12, CMS.

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

Explaining mathematics using formalized mathematics

Hybrid talk (please see abstract for link)

UserProfessor Patrick Massot (Université Paris-Saclay).

House Centre for Mathematical Sciences MR12, CMS.

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

Formalization of diagram chasing as a first-order logic in Coq

Hybrid talk (please see abstract for link)

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

House Centre for Mathematical Sciences MR12, CMS.

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

Smooth vector bundles in Lean

Hybrid talk (please see abstract for link)

UserProfessor Heather Macbeth (Fordham University).

House Centre for Mathematical Sciences MR12, CMS.

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

The Locale-Centric Approach for Formalising Mathematical Hierarchies

UserChelsea Edmonds (University of Cambridge).

House Centre for Mathematical Sciences MR12, CMS.

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

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

[CANCELLED, please check back for rescheduling]

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

House Centre for Mathematical Sciences MR12, CMS.

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

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

Hybrid talk (please see abstract for link)

UserNils Lauermann (INRIA).

House Centre for Mathematical Sciences MR12, CMS.

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

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

UserMantas Bakšys (University of Cambridge).

House Centre for Mathematical Sciences MR12, CMS.

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

Some practical problems in formalising mathematics and how to solve them

Hybrid talk (please see abstract for link)

UserDr Manuel Eberl (University of Innsbruck).

House Centre for Mathematical Sciences MR12, CMS.

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

The Liquid Tensor Experiment

UserProfessor Kevin Buzzard (Imperial College London).

House Centre for Mathematical Sciences MR12, CMS.

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

How Hilbert met Isabelle: Proof Between Generations

Hybrid talk (please see abstract for link)

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

House Centre for Mathematical Sciences MR12, CMS.

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

Formalised Mathematics: Obstacles and Achievements

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

House Centre for Mathematical Sciences MR12, CMS.

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

Please see above for contact details for this list.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity