Two projects proposed by Berkeley EECS professors recently received funding from the AI for Math Fund to develop systems that help advance mathematical discovery and research.
The UC Berkeley College of Computing, Data Science, and Society and the College of Engineering share the Department of Electrical Engineering and Computer Sciences (EECS).
Last week, the AI for Math Fund announced a total of $18 million in grants for 29 projects, one of the largest ever philanthropic commitments supporting the development of AI and machine learning-based tools to advance mathematics. Individual grants range up to $1 million for up to 2 years of work on open-source projects and research. The AI Math Fund is managed by Renaissance Philanthropy in partnership with founding donor XTX Markets.
Vellum project to enable AI-assisted reasoning across math and computer science
Dawn Song, EECS professor and faculty co-director of the Berkeley Center on Responsible, Decentralized Intelligence, is part of a research collaboration between Berkeley and University of Texas at Austin for the Vellum project.
Vellum is a flexible, open-source framework that connects large language models with interactive theorem-provers and automated solvers, and by doing so, enables large-scale, AI-aided formal reasoning for both mathematics and computer science applications.
“This technology not only advances AI for mathematics and formal reasoning, but also supports program verification and the development of safer, more secure systems – an essential foundation for responsible innovation in AI and agentic AI,” said Song.
LeanTutor project to reliably evaluate students’ mathematical proofs
Gireeja Ranade, EECS associate teaching professor, received a grant to develop LeanTutor, an innovative tool to help teach mathematical proofs to undergraduate students.
The LeanTutor tool will aim to reliably evaluate mathematical proof correctness, generate correct next steps and offer tailored guidance to undergraduate students. LeanTutor’s design draws on insights from education research, machine learning and formal methods to develop a system for students and AI agents to meaningfully work on mathematics together.
“I’m especially excited about the team of students – a mix of graduate and undergraduate students from EECS, math and education design – working on this project,” said Ranade. “We’re tackling some fundamental problems in AI for math, and the educational perspective is bringing new ideas.”
Manooshree Patel, EECS graduate student and Berkeley School of Education PhD student, is working on the project with Ranade.
“We are planning to deploy LeanTutor in an upper-division engineering math course taken by hundreds of students at Berkeley this spring,” said Patel. “I am excited for LeanTutor’s potential educational impact in this class, and hopefully more undergraduate math classes in the future, by providing correct, immediate and accessible feedback to every student who needs it.”
