|![[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. Talk recordings can be found on our YouTube channel. 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. 11 upcoming talks and 42 talks in the archive. Decision Procedures for Bitvector Reasoning in Lean
Title to be confirmed
Formalisation of minimum cost flows in Isabelle/HOL
Title to be confirmed
Formalising Brauer Group and Group Cohomology in Lean4
Title to be confirmed
Title to be confirmed
Formal verification of the 5th Busy Beaver value
Title to be confirmed
Title to be confirmed
Title to be confirmed
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. |
Siddharth Bhat (University of Cambridge).
Thursday 23 January 2025, 17:00-18:00