|
15:30-16:45, Seminar Hall Mechanising Mathematics T.V.H. Prathamesh Institute of Mathematical Sciences, Chennai. 16-09-15 Abstract 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 which use computer(Four Color Theorem, Kepler Conjecture 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 a theorem prover called Isabelle.
|
