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