Fwd: Colloquium at TIFR-CAM : Kevin M Buzzard, Teaching proofs to a computer

Skip to first unread message

Siddhartha Gadgil

Apr 21, 2022, 12:09:22 PMApr 21
to automated-mat...@googlegroups.com

---------- Forwarded message ---------
From: Nishant Chandgotia <nis...@tifrbng.res.in>
Date: Thu, 21 Apr 2022 at 8:08 PM
Subject: Colloquium at TIFR-CAM : Kevin M Buzzard, Teaching proofs to a computer
To: <announ...@tifrbng.res.in>


Speaker: Kevin M Buzzard  (Imperial College London)
Date and time: Tuesday, April 26, 2022 4:00 PM

Title: Teaching proofs to a computer.

Abstract: We all know about computer algebra packages like Maple or Matlab, which can be used to do calculations. But there are other computer programs called things like Coq or Lean or Isabelle/HOL, which can be used to check or generate mathematical proofs. Such systems have existed for decades but it is only recently that the research mathematical community have begun to take them seriously. I will give an overview of what has been happening over the last few years, and also why I think it might begin to matter to our community. I don't think that computers will be automatically proving the Riemann Hypothesis any time soon, but I do think that maybe they will soon be able to help us with our research, in areas where Maple and Matlab are no use. I will assume the audience has a basic mathematical background but I will not assume any knowledge of computers or computer proof systems.

There will be snacks and coffee after the colloquium for participants  at TIFR-CAM.
  Meeting ID: 921 0831 2024
  Passcode: B9NUTt


To get on this mailing list please contact either Nishant Chandgotia (nis...@tifrbng.res.in) or Ujjwal Koley (ujj...@tifrbng.res.in). 

Reply all
Reply to author
0 new messages