COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |
Formalisation of mathematics with interactive theorem provers
Add to your list(s)
Send you e-mail reminders
Further detail
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. 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 GeometryArtie 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 Structures in dependent type theoryOnline Professor Jeremy Avigad (Carnegie Mellon University). Live-streamed at MR14 Centre for Mathematical Sciences. Thursday 15 February 2024, 17:00-18:00 How to prove Fermat's Last TheoremOnline Professor Kevin Buzzard (Imperial College London). Live-streamed at MR14 Centre for Mathematical Sciences. Thursday 08 February 2024, 17:00-18:00 Comparative Formalisation of Kneser's theorem in Isabelle/HOL and LeanMantas Bakšys and Yaël Dillies (University of Cambridge). MR14 Centre for Mathematical Sciences. Thursday 01 February 2024, 17:00-18:00 Towards Autoformalization and Mathematical Reasoning using language modelsNote unusual time Professor Siddhartha Gadgil (Indian Institute of Science). MR14 Centre for Mathematical Sciences. Wednesday 17 January 2024, 13:00-14:00 Roth numbers: Upper, lower bounds, and related constructionsNote: different room, MR20 this time Yaël Dillies (University of Cambridge). MR20 Centre for Mathematical Sciences. Thursday 22 June 2023, 17:00-18:00 Formalizing the change of variables formula for integrals in mathlibHybrid 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 Formalizing algebraic number theory, recent progress and future challengesNote: 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 The leanest automataHybrid 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 Formalising Erdős and Larson: Ordinal Partition TheoryProfessor Lawrence C. Paulson FRS (University of Cambridge). Centre for Mathematical Sciences MR12, CMS. Thursday 25 May 2023, 17:00-18:00 Explaining mathematics using formalized mathematicsHybrid 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 Formalization of diagram chasing as a first-order logic in CoqHybrid 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 Smooth vector bundles in LeanHybrid 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 Formalising modular forms, Eisenstein series and the statement of the modularity conjecture in LeanDr Chris Birkbeck (University of East Anglia). Centre for Mathematical Sciences MR12, CMS. Thursday 27 April 2023, 17:00-18:00 The Locale-Centric Approach for Formalising Mathematical HierarchiesChelsea Edmonds (University of Cambridge). Centre for Mathematical Sciences MR12, CMS. Thursday 16 March 2023, 17:00-18:00 [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 Formalising Turán's Graph Theorem in Isabelle/HOLHybrid 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 the Balog–Szemerédi–Gowers Theorem in Isabelle/HOLMantas Bakšys (University of Cambridge). Centre for Mathematical Sciences MR12, CMS. Thursday 23 February 2023, 17:00-18:00 From benchmark-centric to human-centric: deep learning methods in the formalisation of mathematicsAlbert Qiaochu Jiang (University of Cambridge). Centre for Mathematical Sciences MR12, CMS. Thursday 16 February 2023, 17:00-18:00 Some practical problems in formalising mathematics and how to solve themHybrid 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 The Liquid Tensor ExperimentProfessor Kevin Buzzard (Imperial College London). Centre for Mathematical Sciences MR12, CMS. Thursday 02 February 2023, 17:00-18:00 How Hilbert met Isabelle: Proof Between GenerationsHybrid 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 Formalised Mathematics: Obstacles and AchievementsProfessor Lawrence C. Paulson FRS (University of Cambridge). Centre for Mathematical Sciences MR12, CMS. Thursday 19 January 2023, 17:00-18:00 Please see above for contact details for this list. |
Other listsRandomised Algorithms & Processes Bus Booking Martin Centre Research Seminars, Dept of ArchitectureOther talksGateway- CCIMI Plenary Talk: Single versus double interlacing in random tiling models CANCELLED: Post Office Lives: stories of life and death in the British Post Office Measuring emissions by satellite to support the Paris Agreement Locating the Reversals: Adapting EMMA for the screen Generalised hydrodynamics of the KdV soliton gas. |