A Structured Representation of Tactics for Machine-Assisted Theorem Proving
The Project
This project develops a machine learning-driven approach to creating tactics for interactive theorem proving. The project will represent tactics as algebraic objects in a high-level language that, once applied, modify proof states. In turn, this language can be translated into Lean meta-programs, and will facilitates large language models' automatic creation of proof scripts through interactive sessions. Through this work, the project hopes to uncover new proof strategies that can further streamline theorem proving efforts.
The Team
Jules Hedges is a computer scientist and mathematician who is interested in the theory of bidirectional processes and their application to fields such as economics, machine learning and software architecture, known as "categorical cybernetics". They were previously a lecturer at the University of Strathclyde, and postdocs at the Max Planck Institute for Mathematics in the Sciences, Leipzig and the University of Oxford.
Zanzi Mihejevs has over 10 years of experience in formalizing a broad range of categorical structures using functional programming, and a rich history of consulting companies in building domain specific languages. She is a lead researcher and PI the ARIA funded project at Glaive, where she is working on building a programming language that pushes the frontier of programming with category theory.
Dr. Bruno Gavranović is a mathematician and computer scientist who pioneered Categorical Deep Learning through his research with Google DeepMind and his PhD thesis "Fundamental Components of Deep Learning: A Category-Theoretic Approach". He has translated this theoretical work into practical impact by playing a key role in securing $31M in funding for Symbolica AI, and founding Coend, a company developing foundation models tailored for code-generation in programming languages with first-class types.
Andre Videla is a PhD candidate at the University of Strathclyde and researcher at Glaive. His work on containers, interactive systems, and the future of programing lead him to develop and maintain various aspects of the Idris programming language. Andre's work combines abstract categorical thinking with real-world programming expertise to provide new solutions to modern software challenges.
Dylan Braithwaite is currently writing up for his PhD in theoretical computer science. He has experience with the categorical semantics of programming languages and probabilistic programming, and has formerly worked as a software developer. As a member of Glaive he has been working on an Advanced Research and Innovation Agency funded grant, on the implementation of a programming language which more ergonomically represents mathematical structures using categorical structure.