Gireeja Ranade
Gireeja Ranade is an associate teaching professor of electrical engineering and computer sciences at UC Berkeley who builds AI tools for learning mathematical proof. She studied EECS at MIT and Berkeley, finished a Ph.D. with Anant Sahai in 2014, and designed the pilot of Berkeley's EECS 16A and 16B courses before working as a researcher at Microsoft Research AI. In 2017 and 2018, she coauthored papers on imitation learning for robot planning and on testing robot controllers for safety violations. Her LeanTutor system, first posted in June 2025, pairs large language models with the Lean theorem prover to check student proofs, and it received an AI for Math Fund grant in September 2025. Among her honours are the 2017 UC Berkeley Electrical Engineering Award for Outstanding Teaching and a 2023 NSF CAREER award.
Timeline
-
2007–2014
Degrees at MIT and Berkeley
She earns a B.S. in EECS at MIT in 2007 and an M.S. in EECS at UC Berkeley in 2009. Advised by Anant Sahai, she completes her Berkeley Ph.D. in 2014 with the dissertation "Active Systems with Uncertain Parameters: an Information-Theoretic Perspective."
-
2017
The EECS 16A and 16B pilot
As a lecturer in Berkeley's EECS department, she designs and teaches the pilot version of the new lower-division course sequence EECS 16A and 16B. She receives the 2017 UC Berkeley Electrical Engineering Award for Outstanding Teaching.
-
2017–2018
Imitation learning for robot planning
In November 2017, she coauthors "Data-driven Planning via Imitation Learning," which trains robot planning policies by imitating a clairvoyant oracle that knows the full world map. A February 2018 paper with Shromona Ghosh, Felix Berkenkamp, Shaz Qadeer and Ashish Kapoor uses Bayesian optimization to test robot controllers for counterexamples that violate their safety specifications.
-
2021
Teaching professor at Berkeley
After working as a researcher in the Adaptive Systems and Interaction Group at Microsoft Research AI, she joins the Berkeley EECS faculty. As an assistant teaching professor, she wins a UC Berkeley Extraordinary Teaching in Extraordinary Times award in April 2021. For EECS 16A, she and her students build an automated, scalable and inclusive process for forming study groups.
-
2023
An NSF CAREER award
In 2023, the National Science Foundation gives her a CAREER award, with a $519,947 grant to explore new non-linear control strategies. Berkeley also honours her in 2023 with the Faculty Award for Outstanding Mentorship of GSIs.
-
June 2025–March 2026
The LeanTutor paper
In June 2025, she and six coauthors, with Manooshree Patel as first author, present LeanTutor, a tutoring system built on large language models that formally verifies student-written math proofs in Lean, generates correct next steps and gives instructional guidance. The Proceedings of the AAAI Conference on Artificial Intelligence publish the work in March 2026, together with PeanoBench, a dataset of 371 Peano Arithmetic proofs in natural and formal language.
-
September 2025
An AI for Math Fund grant
In September 2025, as an EECS associate teaching professor, she receives an AI for Math Fund grant to develop LeanTutor as a tool for teaching proofs to undergraduates. The fund, managed by Renaissance Philanthropy with founding donor XTX Markets, announces $18 million for 29 projects in September 2025. LeanTutor aims to auto-formalize students' proofs, check them with an interactive theorem prover and offer tailored guidance.
-
As of October 2026
Associate teaching professor at Berkeley
In spring 2026, she is a visiting scientist in the Simons Institute's Federated and Collaborative Learning program. She is an associate teaching professor of EECS at UC Berkeley, with research interests that include artificial intelligence, and in fall 2026 she teaches CS C182, Designing, Visualizing and Understanding Deep Neural Networks.
Sources and credits
Photo: We have no published photo of Gireeja Ranade yet. Send us a free-licensed photo.
- EE Teaching Faculty | EECS at UC Berkeley
- Ranade, Shrivastava, Monga, Yang, Rampure and Shen win Extraordinary Teaching in Extraordinary Times Awards - EECS at Berkeley
- Gireeja Ranade - The Mathematics Genealogy Project
- Gireeja Ranade - Professor UC Berkeley
- Gireeja Ranade
- [1711.06391] Data-driven Planning via Imitation Learning
- [1802.08678] Verifying Controllers Against Adversarial Examples with Bayesian Optimization
- Berkeley engineers win Extraordinary Teaching in Extraordinary Times Awards - Berkeley Engineering
- Two EECS professors recognized with NSF CAREER Awards - Berkeley Engineering
- Gireeja Ranade honored for outstanding mentorship of GSIs - EECS at Berkeley
- [2506.08321v1] LeanTutor: A Formally-Verified AI Tutor for Mathematical Proofs
- LeanTutor: Towards a Verified AI Mathematical Proof Tutor | Proceedings of the AAAI Conference on Artificial Intelligence
- UC Berkeley receives AI for Math Fund grants for Vellum and LeanTutor projects | CDSS at UC Berkeley
- LeanTutor: A tutor for undergraduate mathematics proofs — Renaissance Philanthropy