Ajay Kumar Nair

AKNair

About Me

I am a Postdoctoral researcher in the Department of Mathematics at the Indian Institute of Science Bengaluru, where I work with Prof. Siddhartha Gadgil on LeanAide, a project at the intersection of AI and formal mathematics that explores autoformalisation in Lean. The project is supported by the AI for Mathematics Fund managed by Renaissance Philanthropy and XTX Markets.

My research interests lie in Lean, AI, and autoformalisation, and in low-dimensional geometry and topology. I completed my PhD in mathematics at the Indian Institute of Science Bangalore under Prof. Subhojoy Gupta, with Prof. Gadgil as co-advisor, working on geometric structures on surfaces and their holonomies.

You can find more about my research interests here and my publications here.

My academic CV is available here.

For contact details, please see the contact page.

Current Activities

In April 2026, I will serve as Lead Coordinator and Tutor for the Hackathon: LeanLang for Verified Autonomy, to be held at IISc Bangalore and online, in association with Emergence India Labs.

I contribute to Lean Metaprogramming Recipes, a Lean 4 cookbook of programming and metaprogramming examples, and share a broader record of my work on GitHub.

I also write on CHIAROSCURO, a personal blog of short pieces, reviews, and essays. It is not active at the moment, but it remains part of my writing archive.