Seminar/ Colloquium

Title : Automating Mathematics?
Speaker : Siddhartha Gadgil , IISc
Date : 15/09/2017, Seminar Hall, First Floor.

Abstract: 

As Artificial Intelligence betters human intelligence at a range of tasks, from playing Chess to Quizzing to playing Go, one may hope that computers can play a central role in the discovery and proofs of mathematical results. Indeed, computers are playing various roles in mathematical discovery, from enumeration and SAT solvers being used in proofs, to deduction of results from axioms by automated theorem proving systems. However, their role, so far, has been somewhat peripheral. We will survey some of these methods and their limitations.

The board games Chess and Go are an excellent ground for learning and testing AI systems. I will discuss the evolution of computer systems that play these, especially in the context of lessons towards automating mathematics.

One of the impediments to computer verification and discovery of proofs has been the unsuitability of the usual foundations of mathematics for such a task. Indeed, formal proof systems have used different foundations, but these have other limitations. I will briefly discuss the emerging field called homotopy type theory, based on deep connections discovered between topology and type theory. Homotopy type theory provides much better foundations for mathematics, especially with computer assistance.

Finally, I will briefly discuss some of my own work, which is still in early stages, on using additional forms of learning, including reinforcement learning and natural language processing, to complement the present state-of-the art systems in the quest to enable computers to do mathematics.