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
Jade Master has a Ph.D in applied category theory specialising in the compositionality of complex systems. After a postdoc in coalgebraic formal verification and employment as a functional programmer she is a lead researcher and PI on the ARIA Safeguarded AI project. Her project with ARIA aims to develop scalable world models based on categorical formalisms. She plans on synergising this work with the Containers for AI Project by developing compositional technology for tactic generation.
Vincent Wang-Maścianica obtained his PhD from Oxford, with a research focus on monoidal category theory bridging practical computational semantics and formal compositional structures. He is currently a senior researcher at the Laboratory for Human-Centered AI at the Philosophy Department at 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.