|![[Search]](http://talks.cam.ac.uk/images/search.gif?1209136071)
|![[A-Z Index]](http://talks.cam.ac.uk/images/az.gif?1209136071)
|![[Contact]](http://talks.cam.ac.uk/images/contact.gif?1209136071)
||![[University of Cambridge]](http://talks.cam.ac.uk/images/identifier2.gif?1209136071){kind=small} |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![[Talks.cam]](http://talks.cam.ac.uk/images/talkslogosmall.gif?1209136071) |
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; Bhavik Mehta; Angeliki Koutsoukou-Argyraki; Mantas Bakšys. If you have a question about a specific talk, click on that talk to find its organiser. 8 upcoming talks and 9 talks in the archive. The Locale-Centric Approach for Formalising Mathematical Hierarchies
[CANCELLED] Real Closed Field and Thom Encoding in Isabelle/HOL[CANCELLED, please check back for rescheduling]
Formalising Turán's Graph Theorem in Isabelle/HOLHybrid talk (please see abstract for link)
Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
From benchmark-centric to human-centric: deep learning methods in the formalisation of mathematics
Some practical problems in formalising mathematics and how to solve themHybrid talk (please see abstract for link)
The Liquid Tensor Experiment
How Hilbert met Isabelle: Proof Between GenerationsHybrid talk (please see abstract for link)
Formalised Mathematics: Obstacles and Achievements
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. |
Chelsea Edmonds (University of Cambridge).
Thursday 16 March 2023, 17:00-18:00