![[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)
Professor Lawrence C. Paulson FRS (University of Cambridge).
Thursday 25 May 2023, 17:00-18:00
Centre for Mathematical Sciences MR12, CMS
Contact: No managers listed
0 upcoming talks View 18 archived talks
Formalisation of mathematics with interactive theorem provers
Formalising Erdős and Larson: Ordinal Partition Theory
Formalisation of mathematics with interactive theorem provers
Explaining mathematics using formalized mathematics
⚠️ Hybrid talk (please see abstract for link)
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)
Formalisation of mathematics with interactive theorem provers
Smooth vector bundles in Lean
⚠️ Hybrid talk (please see abstract for link)
CCIMI Seminars
Fundamental limits of generative AI
Formalisation of mathematics with interactive theorem provers
Formalising modular forms, Eisenstein series and the statement of the modularity conjecture in Lean
Formalisation of mathematics with interactive theorem provers
The Locale-Centric Approach for Formalising Mathematical Hierarchies
Formalisation of mathematics with interactive theorem provers
[CANCELLED] Real Closed Field and Thom Encoding in Isabelle/HOL
⚠️ [CANCELLED, please check back for rescheduling]
Formalisation of mathematics with interactive theorem provers
Formalising Turán's Graph Theorem in Isabelle/HOL
⚠️ Hybrid talk (please see abstract for link)
Formalisation of mathematics with interactive theorem provers
Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
Formalisation of mathematics with interactive theorem provers
From benchmark-centric to human-centric: deep learning methods in the formalisation of mathematics
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)
Formalisation of mathematics with interactive theorem provers
The Liquid Tensor Experiment
Formalisation of mathematics with interactive theorem provers
How Hilbert met Isabelle: Proof Between Generations
⚠️ Hybrid talk (please see abstract for link)
Formalisation of mathematics with interactive theorem provers
Formalised Mathematics: Obstacles and Achievements
Worms and Bugs
What activity types posed the greatest risk of SARS-CoV-2 infection for a university community?
Worms and Bugs
Modelling the impact of asymptomatic testing and isolation policies on SARS-CoV-2 transmission in workplaces
Worms and Bugs
SARS-CoV-2 evolution: (Dis)entangled on multiple scales
Please see above for contact details for this list.