LeanTutor

A Tutor for Undergraduate Mathematics Proofs

The Project

LeanTutor revisits the way undergraduate students learn mathematical proving with the help of interactive theorem provers (ITPs) and large language models (LLMs). LeanTutor aims to auto-formalize students' (undergraduate-level) natural language proofs, evaluate proof correctness using an ITP, use feedback from the ITP to generate subsequent steps, and offer tailored guidance to students. LeanTutor's design draws on insights from education research, machine learning, and formal methods to develop a system for students and artificial intelligence (AI) agents to meaningfully work on mathematics together.

The Team

Gireeja Ranade is an Associate Teaching Professor in Electrical Engineering and Computer Sciences (EECS) at the University of California, Berkeley. Before this, she was a Researcher at Microsoft Research in Redmond, WA. She received her PhD in Electrical Engineering and Computer Science from the University of California, Berkeley, and her undergraduate degree from MIT in Cambridge, MA. She is the recipient of multiple awards for her research and teaching such as the NSF CAREER Award, the UC Berkeley Electrical Engineering Award for Outstanding Teaching, the UC Berkeley Award for Outstanding GSI Mentoring and others.