Advancing mathematics and formal methods with frontier AI.
gAnIt is the flagship programme of Emergence India Lab. It supports a distributed network of research clusters across India's leading mathematics groups, each using frontier AI to work on problems in mathematics and formal methods — and to bring AI into the everyday practice of mathematical research.
Over the past year, AI systems have moved from assisting mathematicians to taking part in the research itself — proposing arguments, searching for counterexamples, and helping produce proofs that are written in formal systems like Lean and checked by the wider community. The supporting tools — proof assistants, autoformalization, and model-guided search — have matured enough for serious mathematical work.
India has world-class mathematics groups. What has been harder to come by is dependable access to frontier models and the engineering that surrounds them. gAnIt exists to close that gap — and to do it in the open.
This is an early but real opportunity. AI is making genuine progress on problems that are within reach today, even as the deepest questions in mathematics remain far off. gAnIt is built for solid, verifiable work that the wider community can check and build on — not for overstating what is possible.
The programme supports a distributed network of clusters across India's mathematics groups. Each cluster works at its home institution and publishes openly, keeping full authorship and academic credit. Clusters run independently but stay connected — sharing progress, tools, and techniques, and helping one another along the way. Progress is reviewed individually, in a developmental spirit, and the design is deliberately light.
It sets the frontier themes, selects clusters, convenes the quarterly review, and stewards the open-research framework that holds the network together.
One or more researchers or professors — with their students or postdocs where relevant — working on a defined theme at their home institution, led by a named Cluster Lead and reviewed individually on their own evidence.
Access to frontier models, and possible collaboration with Emergence's researchers on the skills, tools and pipelines on autoformalization, proof assistants, and agentic verification — together with light-touch support.
Within a set of agreed frontier themes, each cluster proposes and pursues its own problems — the ones where it sees the clearest opportunity. Well-justified adjacent directions are welcome too.
We're inviting proposals from mathematics groups across India. Tell us who you are and the theme you would pursue, and we'll take it from there.