Sketchpad
A High-Precision and Easy-to-Use System For Automatic Formal Sketch Generation
The Project
Sketchpad is an AI-powered system for converting natural language proofs into structured formal sketches, designed to assist formal mathematics practitioners working in both Isabelle and Lean. By introducing a graph-based representation, it enables proofs to be decomposed into individual statements, supporting fine-grained autoformalisation and more effective interaction with partial or incomplete proofs.
The Team
Wenda Li is an Assistant Professor in Hybrid AI at the University of Edinburgh, specialising in AI for mathematics. He has contributed to pioneering work on autoformalisation using large language models and explored approaches for guiding formal theorem proving with informal proofs. Beyond this, his work also spans verified quantifier elimination, Grothendieck’s scheme theory, and aspects of analytic number theory. His achievements in these areas were recognised as a runner-up for the BCS Best Dissertation Award.
Luo Mai is an Associate Professor at the University of Edinburgh, where he leads the Large-Scale Machine Learning Systems Group. He serves as Co-Director of the UK EPSRC Centre for Doctoral Training in Machine Learning Systems and Co-Lead of a UK ARIA project, Scaling Compute – Charting the Course. His research covers computer systems, machine learning, and data management. He has led the development of AI systems that have been adopted by major technology companies and widely released as open-source software with substantial uptake. He is a recipient of the Google Doctoral Fellowship and the Microsoft Research Asia StarTrack Award, and was a finalist for the Chancellor’s Rising Star in Research award.
Larry Paulson is an Amazon Scholar and Emeritus Professor of Computational Logic at the University of Cambridge and a renowned expert in formal logic and proof assistants. He led the development of the widely used Isabelle proof assistant and pioneered Sledgehammer, a groundbreaking innovation that has been adopted by nearly all major proof assistants. In recognition of his significant contributions to proof assistants and automated reasoning, he has been elected an ACM Fellow, a Fellow of the Royal Society, and has received the Herbrand Award.
Huajian Xin is a PhD student at the University of Edinburgh, working with Jacques Fleuriot and Wenda Li. His research focuses on automated theorem proving using large language models, with an emphasis on autonomous agents capable of autoformalisation and knowledge base learning. His representative works include: the state-of-the-art open-source theorem proving models DeepSeek Prover series; LEGO-Prover, which features task decomposition and knowledge accumulation; and APE-Bench, a benchmark dataset for library-scale proof engineering evaluation.