Formalizing A-infinity category theory in Lean
Mina Aganagic, Professor
Mathematics
Applications for Spring 2026 are closed for this project.
Today’s gold standard for establishing new theoretical results in mathematics is an accompanying formal computer-verification of the main theorems and their proofs (see reference below). Systems known as interactive theorem provers (ITPs), first designed to formally verify computer algorithms, have recently gained significant momentum in many mathematics communities. These ITPs, like Isabelle, Rocq or Lean, offer a formal language that mechanizes reasoning and can be used to implement algorithms, mathematical functions, and general-purpose proofs. In 2024, Google DeepMind used reinforcement learning in Lean to win a silver medal in the International Mathematics Olympiad for the first time.
In our research group, we develop cutting-edge mathematics that connects topology, geometry and algebra based on physical intuition. For this project, we work on distinguishing mathematical knots with so-called knot invariants, which are defined using algebra & category theory. Because of the geometrical and physical setup of this definition, a special kind of category known as an A-infinity category is required for our calculations. Traditionally, these methods have often been obscured by abstraction, but we are pioneering a concrete, tractable algorithm.
The goal of this project is to implement said algorithm in the formal language of Lean. Rather than just doing calculations, the Lean language will allow us to reason about its properties and to do research-level mathematics in true interaction with the computer. Contemporary results from this field have never been formalized previously. Libraries of formalized mathematics (like Lean’s mathlib) provide unified, searchable and cross-linked databases of mathematical knowledge. This also allows training artificial intelligence models in an environment where precise details matter. Above all, the narrow initial scope and immediate feedback by the software turns abstract mathematics especially accessible for a URAP project.
Role: The student will begin by developing the foundational definitions and theorems of A-infinity category theory using the Lean theorem prover. This process will involve many concrete design decisions within the constraints of Lean’s dependent type theory, on which we will work together. It would be ideal to then instantiate these definitions with examples motivated by the research program above. Depending on progress, the student could then proceed by extending this library in a direction of their own interest, with possibilities in geometry, knot theory and representation theory. The results of this project should be contributed to Lean’s mathlib as a pull request.
Qualifications: Students majoring in mathematics, computer science, data science, physics or any related fields are welcome to apply. A first course in abstract algebra as well as programming experience is preferable. Additional background in category theory or any interactive theorem prover is a plus. Previous research experience is not required.
Day-to-day supervisor for this project: Marco David
Hours: to be negotiated
Related website: https://doi.org/10.1090/noti2860
Mathematical and Physical Sciences