Automated Theorem Proving Explained | Seminar Saturdays @ IIITH

In this video, Anurudh gives a brief introduction to formally verified mathematics, and motivates why we need it. He describes what Theorem Provers or Proof Checkers are, and discusses a special class of them called Interactive Theorem Provers or Proof Assistants. We'll look at some examples of theorems that have been verified by computers. And then dive a little into how you teach a computer math. We'll explore the equivalence between mathematical proofs and computer programs, and how to represent them. Speaker: Anurudh Peduri Resources: 1. He primarily Coq (https://coq.inria.fr/) and Lean (https://leanprover.github.io/) for the talk. 2. Heavily inspired by https://xenaproject.wordpress.com/what-is-the-xena-project/ 3. Curry - Howard (https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence) https://iiittheorygroup.github.io/Initiatives/Seminar-Saturdays/Past-Talks/006