Alladi Ramakrishnan Hall

Mechanising Mathematics: Excursions in Interactive Theorem Proving

T V H Prathamesh

IMSc

Mechanisation of Mathematics refers to the use of computers to generate or
check mathematical proofs. An interactive theorem prover is a software tool
which partly automates and checks such 'proofs' by human-machine
collaboration. The potential impact of recent developments in interactive
theorem proving on the practice of everyday mathematics range from their use in verification of mathematical proofs (Kepler's Conjecture/Theorem, Four Color Theorem and Feit Thompson theorem) to a renewed interest in logical foundations of mathematics (Homotopy Type Theory by Voevodsky et al). In this talk, I intend to present a brief survey of the history and current developments in interactive theorem proving, while simultaneously addressing questions about necessity and importance of such an endeavor. I intend to present a working demonstration of an interactive theorem prover called Isabelle, and briefly discuss my related work about formalization of results in knot theory in Isabelle/HOL.