Siddhartha Gadgil,
Department of Mathematics,
Indian Institute of Science.
Bangalore 560012, India
E-mail: siddhartha[dot]gadgil[at]gmail[dot]com

Education and Employment

  • Bachelor of Statistics, Indian Statistical Institute, Calcutta, 1995.
  • Ph. D., California Institute of Technology, (thesis advisor: David Gabai) 1999.
  • Simons Instructor, Stony Brook University, 1999-2002.
  • Associate Professor, Indian Statistical Institute, Bangalore, 2002-2006.
  • Associate Professor, Indian Institute of Science, Bangalore, 2006-20012.
  • Professor, Indian Institute of Science, Bangalore, 2012 onwards.



Past courses

The following are some of the courses that I have taught recently.


My research started in (Low-dimensional) Topology and I have worked for many years in this and related areas, including Geometric group theory, Riemannian geometry and Metric geometry (and its relation to Probability Theory). I also briefly worked on an application of topology to Molecular Biology.

More recently, the main focus of my work has been automated theorem proving, i.e., trying to get computers to do mathematics. The one success so far has been the PolyMath 14 project, which resulted in the publication Homogeneous length functions on groups whose discovery involved a computer proof, an account of which is published in the Journal of Automated Reasoning.

I also occasionally blog about my experiments with automating mathematics.

Publications and Preprints

Most of my publications are available on MathSciNet (needs subscription). Most publications and preprints are available on the arXiV.


My main (till about an year ago) automated theorem proving activity is open sourced at ProvingGround on GitHub, consisting mainly of scala code.

More recently, I have focussed on working with Lean Prover 4, using it as a programming language and a theorem prover working together seamlessly. Some of my projects with these are the following:

  • Polylean containing Gardam's disproof of Kaplansky's conjecture (with Anand Rao Tadipatri) as well as lean replication of the PolyMath code.
  • Lean-loris: Metaprogramming in lean 4 for forward reasoning and other applications.
  • Saturn: A SAT solver-prover in lean 4.
All these are described in my blog.

Various other pieces of software are on Github. One of these, Superficial, is an ongoing attempt at building a library to work with surfaces and structures on them.

Ph.D. students guided

I have guided seven Ph.D. students, plus one informally, all of whom have faculty positions at excellent places. They are: Tejas Kalelkar (IISER, Pune), Suhas Pandit (IIT Madras), Dheeraj Kulkarni (IISER Bhopal), Bidyut Sanki (IIT, Kanpur), D. Divakaran (Azim Premji University), T.V.H.Prathamesh (KREA University), Arpan Kabiraj(IIT Palakkad) and (informally) Dishant Pancholi (IMSc Chennai).


Some of the presentations I have made over the years using slides are below. The slides using reveal.js are viewable on the web and mobile friendly.

Online Expositions and Demos

Expository articles

For a general scientific audience.

More technical

Siddhartha Gadgil