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.

Courses

Current/Upcoming

• MA 332: Algebraic Topology, January 2024.

Past courses

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

• MA 232: Introduction to Algebraic Topology, August 2023.
• MA 208: Proofs and Programs, January 2023.
• MA 231: Topology, August 2022.
• MA 332: Algebraic Topology, January 2022.
• MA 231: Topology, August 2021.
• MA 232: Introduction to Algebraic Topology, October 2020.
• Algebraic Topology, January 2020.
• Computer-Assisted Topology and Geometry, January 2020.
• Introduction to Algebraic Topology, August 2019; earlier taught in August 2016.
• TrainLogic, an introduction to logic and type theory as background material for formal methods for a software group from Alstom.
• Logic, Types and Spaces, January 2019; earlier taught in January 2015.
• Probability Models, August 2019.
• Analysis and Linear Algebra II, January 2018.
• Introduction to Homotopy Type Theory, January 2017.
• Basic Analysis, January 2016.
• Elementary Algebra and Number Theory, January 2014.
• Mathematical Logic and Computability, August 2012.
• Algebraic Topology, I used a tablet and saved whiteboard notes in January 2011 and January 2010 (to be viewed in landscape mode).

Research

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 work with Anand Rao Tadipatri on Gardam's disproof of Kaplansky's conjecture was published in Certified Programs and Proofs 2024: final version of the paper.

Software

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:

• LeanAide AI tools to work with the Lean Theorem Prover for auotoformalization as well as attempts at proof discovery.
• 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.

My main automated theorem proving activity before switching to Lean 4 is open sourced at ProvingGround on GitHub, consisting mainly of scala code.

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

Presentations

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.

• A public lecture on Automating Mathematics? as part of the ICTS Kaapi with Kuriosity series. The video and slides are available.
• Another lecture on Automating Mathematics? at a conference organized by the Kerala School of Mathematics (KSOM), aimed at a Mathematical audience. The video and slides are available.
• A lecture on Random words in free groups, non-crossing matchings and RNA secondary structures at the Virtual Math Fest 2020. The video is available.
• I have given a few talks recently on Homogeneous lengths on free groups and the associated computer proof during the PolyMath 14 project.
  • Lengths on Free groups (pdf), lecture at TIFR, Mumbai and a topology conference hosted by IISER, Pune.
  • Homogeneous length functions on Groups: A PolyMath adventure (pdf), lecture at NISER, Bhubaneshwar.
  • Free groups, lengths and computer proofs (reveal.js), lecture at IISER, Thiruvananthapuram.
  • Homogeneous length functions on groups: A PolyMath adventure (reveal.js), lecture at Ashoka University and NEHU, Shillong.
• A few lectures have been on the theme of Automating Mathematics, sometimes overlapping with the PolyMath work.
  • Automating Mathematics: PolyMath, Type Theory and Learning (reveal.js), and accompanying video on YouTube, lecture at CSA Undergraduate Summer School, IISc.
  • Automating Mathematics? (reveal.js), lecture at NCBS, Bangalore.
  • Automating Mathematics? (pdf), lecture at ISI, Bangalore.
• Homotopy Type Theory (reveal.js), lectures on Homotopy Type Theory at Chennai Mathematics Institute and a topology conference in Goa.
• Can computers conquer mathematics? (reveal.js) Another lecture mostly on Homotopy type theory at Microsoft Research, Bangalore.
• String Topology and Geometric Decompostions of 3-dimensional Manifolds (pdf), lecture at East Asian Topology Conference, IISER Mohali.
• The Goldman bracket characterizes homeomorphisms (pdf), lecture at in-house symposium of Mathematics, IISc.
• RNA secondary structures, Linking numbers and Allostery (powerpoint), lecture at National Frontiers of Science symposium, New Delhi.
• Symmetries of Spheres (pdf), lecture at the Indian Academy of Sciences annual meeting, BHU.

Online Expositions and Demos

• I made a few illustrations for a Probability Models course, for example on Markov Chains. Links to other illustrations are on that page.
• Tower of Hanoi live solver.
• I have created an online mini-course on Hyperbolic geometry and Geometric group theory using google's course builder.
• Screencast on Stalling's topological proof of Grushko's theorem and its part two and part three .
• Screencast on Topological rigidity and the Goldman bracket.
• Screencast on Virtual Classification of three-dimensional manifolds.

Expository articles

For a general scientific audience.

• Euclidean Geometry by high-performance solvers? (joint with Anand Tadipatri), experiments in computer proofs, published in Resonance.
• Playing dice with primes., ramblings inspired by Yitang Zhang's work.
• Automating Mathematics?, a piece for a supplement in the Hindu newspaper.
• Ricci flow and the Poincare conjecture : joint with Harish Seshadri.
• Dynamics on the circle : article in Resonance.
• Symmetries of spheres : PDF slides for a lecture to the Indian Academy of Sciences (not designed to be self-contained).
• Chern and total curvature , article in Resonance.

More technical

• A topological characterisation of hyperbolic spaces (following Bowditch).
• Knotted Tori.
• Lectures notes on 3-manifold topology: Connected sums and prime decompositions, Heegaard splittings and Dehn surgery .
• Lecture notes on delta-hyperbolic spaces