Machine Learning for Automated Theorem Proving

Currently, most AI tools for mathematics work essentially as LLM copilots: language models propose proof steps from text, with no built-in grasp of the objects or the domains they reason about. We hope to build more efficient neural architectures built on bespoke mathematical representation spaces, drawn from categorical structures of type theory, which encode the structural symmetries of the underlying mathematical structure of the objects and domains they reason about in a way that is integrated with proof assistants at both the front-end (e.g. tactics) and the back-end (kernel checking, compilation in the learning loop).