Seminar: Mechanized and Automated Theorem Proving

Providing formal mathematical proofs stands as the gold standard and the most reliable method known for ensuring the correctness of statements and improving the knowledge base. Mathematicians and computer scientists widely apply rigorous proofs to guarantee the correctness of their scientific claims, i.e., theorems.

Rigorous proofs consist of a sequence of well-defined, sound reasoning steps. Even though individual steps are simple and easy to check, as the knowledge base expands, proofs become longer, more complex, and harder to understand and verify. Hence, pen-and-paper proofs might contain subtle errors that are hard to find, even by expert mathematicians.

Since reasoning steps in a proof are formally and precisely defined, proof steps can be mechanized and verified using programs called theorem provers. Theorems proven by these programs are free from human errors. Moreover, the theorem prover program might itself help in finding the reasoning steps and completing proofs.

In recent years, theorem provers have shown significant improvements in their capability and begun to attract the attention of researchers who aim for the utmost guarantees. Using theorem provers, mathematicians prove their theorems and find errors in the proofs of famous theorems that have been studied for decades by numerous domain experts. Moreover, computer scientists use theorem provers for formally verifying the correctness of their algorithms and developing reasoning mechanisms on different computational semantic models.

This talk will provide a brief introduction to theorem provers: what they are, how they work, and how they can be used in some research fields. I will also present sample and impactful use cases from mathematics, computer science, and my own research.