Angeliki Koutsoukou-Argyraki (Jan 12 2024 at 14:35): Angeliki Koutsoukou-Argyraki (Jan 12 2024 at 14:35):Dear all,
The seminar series "Formalisation of mathematics with interactive theorem provers" hosted at the Cambridge Centre for Mathematical Sciences that was running last year will be resuming from next week on with Anand Rao Tadipatri and Jonas Bayer @Jonas Bayer taking over the main organisation.
Some meetings will be in person, but whenever the speaker is remote, it will be possible to participate virtually too.
Some of the in-person meetings will be live streamed as well.
This is a joint seminar series between the Cambridge 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.
You can find the schedule (in progress) and relevant information at the link below
http://www.talks.cam.ac.uk/show/index/164015
Please feel free to invite your students and any colleagues who may be interested.
Hope to see many of you!
Angeliki Koutsoukou-Argyraki (Feb 15 2024 at 11:22):We are very excited to host Jeremy Avigad at the Cambridge formalisation seminar today (remotely, at 17:00 UK time) who is going to talk on "Structures in dependent type theory"
https://talks.cam.ac.uk/talk/index/210391
Everyone is welcome!
Angeliki Koutsoukou-Argyraki (Feb 22 2024 at 11:20):Another exciting talk at the Cambridge formalisation seminar
today at 17:00 UK time: "Experiences with Isabelle/HOL: Formalising Real Algebraic Geometry" by Artie Khovanov, Michael Nedzelsky and Wenda Li @Wenda Li (hybrid)
https://talks.cam.ac.uk/talk/index/211648
Angeliki Koutsoukou-Argyraki (Mar 06 2024 at 13:17):Lawrence Paulson @Lawrence Paulson speaking tomorrow at the Cambridge formalisation seminar (hybrid) at 17:00 UK time: "Formalising (part of) the Diagonal Ramsey Paper"! https://talks.cam.ac.uk/talk/index/210400
Looking forward, everyone welcome!
Angeliki Koutsoukou-Argyraki (Apr 23 2024 at 00:24):The Cambridge formalisation seminar
is resuming on April 25th with an online talk by Mohammad Abdulaziz
@Mohammad Abdulaziz
"Formalising Theory of Combinatorial Optimisation" at 5pm UK time: https://talks.cam.ac.uk/talk/index/210877 Everyone welcome!
Angeliki Koutsoukou-Argyraki (Apr 26 2024 at 12:52):Michael Douglas from Harvard University will be giving an in-person talk (which will also be livestreamed!) within the Cambridge "Formalisation of mathematics with interactive theorem provers" seminar series this Monday at 14:00-15:00 (please note the unusual day and time): "Can a computer judge interestingness? "Mathematics is made up of provable interesting statements about numbers, geometry and abstract structures. While proof can be precisely defined, interestingness remains mysterious, a matter of intuition. In this talk we discuss ways to implement interestingness on a computer, both in symbolic and formal terms, and using state of the art AI." https://talks.cam.ac.uk/talk/index/216169 Everyone welcome!
Angeliki Koutsoukou-Argyraki (May 01 2024 at 13:05):Tomorrow at the Cambridge joint formalisation seminar @FacultyMaths @Cambridge_CL we are very happy to host Johan Commelin: "Condensed Type Theory" (5-6 pm UK time)
https://talks.cam.ac.uk/talk/index/212212
Everyone welcome!
Last updated: May 04 2024 at 01:06 UTC