Moving beyond individual proofs to explore the ideas that connect mathematical problems.
Mathematical breakthroughs often come from finding a common idea that connects seemingly different problems. A new research project led by Işil Dillig, professor and chair of the Department of Computer Science at The University of Texas at Austin, aims to help artificial intelligence uncover those connections.
Dillig and collaborator Osbert Bastani, an associate professor at the University of Pennsylvania, have been selected for support from the AI for Math Fund for their project, “Learning Reusable Mathematical Structure in Formal Proofs.” Their proposal was among just 22 selected from more than 470 submissions in a competitive funding round announced by Renaissance Philanthropy and XTX Markets.
The recognition supports research into a central challenge for AI-assisted mathematics: moving beyond proving individual theorems toward discovering ideas that make many results easier to understand, prove and reuse.
Throughout the history of mathematics, new organizing concepts have opened entire fields of discovery. Dillig and Bastani’s project will explore whether AI can learn reusable mathematical structures from existing collections of formal proofs, helping it approach new problems with a broader set of tools.
“Today, AI systems are becoming increasingly good at proving individual theorems, but discovering the underlying concepts that make those proofs possible is a much harder challenge,” said Dillig. “Our goal is to develop AI systems that can identify and reuse these deeper mathematical structures rather than simply automate proofs. I am excited that the AI for Math Fund is supporting this direction.”
The team will develop a framework that combines AI with formal reasoning, using Lean, a software system that checks mathematical proofs for logical correctness. The framework will identify potential structures and characterize them through verified mathematical statements and reusable proof strategies.
The researchers will then integrate those structures into AI-guided theorem provers and evaluate whether they are mathematically meaningful and improve the systems’ ability to prove additional results.
The project builds on Dillig’s work at the intersection of formal methods, programming languages and artificial intelligence. She leads UT Austin’s UToPiA research group and has previously received the ACM SIGPLAN Robin Milner Young Researcher Award, an NSF CAREER Award and a Sloan Research Fellowship.
Through the AI for Math Fund, Renaissance Philanthropy and XTX Markets support projects with the potential to advance mathematical discovery across the field. Dillig’s selection recognizes an ambitious research direction: helping AI discover reusable ideas that could support future mathematical breakthroughs.
Explore more accolades celebrating the achievements of UT Austin’s computer science faculty, students and researchers.