The School of Computer Science, here at the University of Sheffield, is leading a new international project, worth c. $1M in total funding, supported through the AI for Math Fund, managed by Renaissance Philanthropy in partnership with founding donor XTX Markets.
The project, titled ‘Copilots for Isabelle: Learning Logical Structure for a Better Proving Experience’, will advance the foundations and technology of interactive theorem proving, developing next-generation methods for proof assistants. Isabelle/HOL, one of the major proof assistants, will serve as the main platform for innovation. It will deliver new tools for users and developers, and open new research directions in proof mining, program synthesis, and AI-supported reasoning.
Headed up by Dr Andrei Popescu (Principal Investigator and lead for the three-institution collaboration), with Professor Nikos Aletras as Sheffield Co-Investigator. It provides a strong platform for collaboration across Sheffield’s Foundations of Computation, Security of Advanced Systems, and Natural Language Processing research groups, and with research teams at the University of Copenhagen (led by Dr Dmitriy Traytel) and King’s College London (led by Dr Mohammad Abdulaziz).
Speaking about the project, Dr Popescu said:
"Proof assistants are today’s most rigorous tools for formalising mathematics and verifying the correctness of software and hardware systems. In principle, they leave no room for error, since every claim must be reduced to its bare logical core. Their potential is enormous, but adoption has been slow, largely because developing fully formal proofs remains extremely demanding.
"My research has focused on making proof assistants more adaptable to user needs by enabling them to learn highly structured information (organised through the apparatus of category theory) distilled from previous definitions and proofs. By contrast, machine learning methods emphasise flexibility, often working with weaker or implicit structure in the data. This has led to impressive advances with large language models (LLMs), but at the cost of less transparency and reliability -- limitations that are problematic for formal verification.
"In this project, I am working with colleagues in mathematics, formal methods, machine learning, and natural language processing towards a new generation of proof assistants: systems that emulate the versatility of LLMs while internally retaining extreme logical rigour."
The AI for Math Fund, managed by Renaissance Philanthropy in partnership with founding donor XTX Markets, has announced a total of $18 million in grants, one of the largest ever philanthropic commitments supporting the development of AI and machine learning-based tools to advance mathematics. The Fund’s first 29 winning projects include mathematicians and researchers at universities and organizations working to develop systems that help advance mathematical discovery and research across several key tasks.