#### 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.

Done