LeanAide
For Bridging AI and Mathematics with Autoformalization
This project looks to revisit the way mathematical concepts are formalized and discovered by developing a suite of tools that seamlessly integrate natural language processing, large language models (LLMs), and Lean. By creating an accessible, no-code AI+Lean environment, the project seeks to simplify the formalization process for Lean users and empower mathematicians with new, innovative tools for research, including agentic solutions.
The Project
The Team
Siddhartha Gadgil is a Professor of Mathematics at the Indian Institute of Science. He obtained a PhD from Caltech in Geometric topology and worked in related areas for several years. For about a decade he has focussed mainly on Automated Theorem Proving. In the last three years or so, he has worked with the Lean Prover especially towards building tools to integrate with AI. His main research goal is to enable the use AI and Lean for mathematical discovery without requiring any special (non mathematical) expertise.
Viraj Kumar is a Visiting Professor at the Kotak-IISc AI-ML Centre. His research focuses on computing education, with emphasis on rethinking pedagogy and assessment for the Generative AI era. He holds a PhD in Computer Science from the University of Illinois at Urbana-Champaign (2007), and he is an elected member of the ACM India Council, co-chairing its educational initiatives.
Anirudh Gupta is currently pursuing his B.Tech at IISc Bengaluru. His interests lie in mathematics, computer science, and playing the Indian classical flute. A dedicated and passionate individual, he enjoys working with his team, putting effort into his work to the best of his time and abilities. Engaging in research work is not just a professional pursuit for him but a genuine passion that fuels his intellectual curiosity. Eager to contribute meaningfully, he thrives in the academic environment, constantly seeking opportunities for exploration and discovery.
Mrigank is a rising senior at the Indian Institute of Science pursuing a B.Tech. in mathematics and computing. His research is focused on developing tools for improving software quality and automating software engineering processes. In particular, he is interested in exploring the application of traditional software testing and analysis techniques in combination with increasingly capable large language models to solve such problems at scale. With theorem provers that blur the lines between mathematics and software, Mrigank hopes to bring advancements in software engineering to the growing area of formal and automated mathematics.
Swarnava Chakraborty is currently studying B.Tech in Mathematics and Computing at IISc. He has completed his 2nd year. He has always been interested in the field of automated theorem proving. His main research interests lies in autoformalisation using Lean and integration of Artificial Intelligence in this vast field.
Shubham Kumar specializes in Functional Programming with OCaml and Formal Verification using Coq. His interest in formal methods began during his studies and solidified through his work on Multicore OCaml. This experience propelled him toward developing systems in OCaml and applying formal verification techniques with Coq and coq-of-ocaml.