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!
Angeliki Koutsoukou-Argyraki (May 16 2024 at 09:57):Today Thursday 5pm UK time at the Cambridge formalisation seminar
"Teaching using a proof assistant and controlled natural language" by Patrick Massot (Université Paris-Saclay & Carnegie Mellon University)
https://talks.cam.ac.uk/talk/index/215755 Everyone welcome!
Angeliki Koutsoukou-Argyraki (May 23 2024 at 13:53):Georges Gonthier (INRIA) to speak at the Cambridge formalisation seminar today Thursday at 5pm UK time (online)
https://talks.cam.ac.uk/talk/index/216109 "Little Theories for Big Formal Proofs" -Everyone welcome!
Angeliki Koutsoukou-Argyraki (Jun 11 2024 at 12:30):Tobias Nipkow (Munich) @Tobias Nipkow is speaking at the Cambridge formalisation seminar this Thursday at 5pm UK time "Alpha-Beta Pruning Explored, Extended and Verified https://talks.cam.ac.uk/talk/index/216049 Everyone welcome!
Angeliki Koutsoukou-Argyraki (Oct 08 2024 at 17:22):The seminar series "Formalisation of mathematics with interactive theorem provers"
hosted at the Cambridge Centre for Mathematical Sciences is resuming. There will be both in-person and online talks, every Thursday at 17:00-18:00 UK time.
The first talk of the term will take place this Thursday 10 October, and it will be by Maximilian Doré (University of Oxford)
on Cubical Type Theory: "Reasoning with Kan fillings about Morse reductions":
https://talks.cam.ac.uk/talk/index/222244
This is a joint seminar series between the Cambridge Department of Computer Science and Technology and the Faculty of Mathematics.
You can find the schedule (in progress) and relevant information at the link below:
https://talks.cam.ac.uk/show/index/164015
Please feel free to invite your students and any colleagues who may be interested.
All levels welcome. Undergraduate students are particularly encouraged to actively participate.
For any questions or talk suggestions, please contact me or my co-organisers Anand Rao Tadipatri and Jonas Bayer @Jonas Bayer
Last updated: Dec 22 2024 at 08:21 UTC