Bridging Proof and Computation
For a Verified Lean–Macaulay2 Interface
The Project
The project focuses on developing an extensible, native interface between Lean and the computational algebra system (CAS) Macaulay2 (M2) to enhance the integration between CAS and formal proof verification. By creating a Lean-based domain-specific language (DSL) for interacting with M2, the team aims to enable seamless bidirectional communication, allowing Lean users to call M2 functions and M2 users to generate Lean proofs. This initiative will also look to formalizes key algorithms in M2 and explores the development a general computer algebra system (CAS) interface for Lean, potentially benefiting other CAS systems in the future.
The Team
Matthew Ballard studied mathematics at Caltech as an undergraduate and completed his PhD at the University of Washington, Seattle, WA, USA. After postdoctoral appointments at the University of Pennsylvania, Philadelphia, PA, USA; the University of Wisconsin-Madison, Madison, WI, USA; and the University of Vienna, Vienna, Austria, he joined the faculty at the University of South Carolina, Columbia, SC, USA, where he is now a Professor in the Department of Mathematics. His research interests include derived categories across mathematics and the formalization of mathematics. He serves as one of the maintainers of Mathlib, the main mathematics library for the Lean theorem prover.
Anton Leykin studied mathematics at Kharkiv University, Kharkiv, Ukraine, as an undergraduate and defended his PhD at the University of Minnesota, Twin Cities, MN, USA. After postdoctoral appointments at the University of Illinois at Chicago, IL, USA, and the Institute for Mathematics and its Applications, Minneapolis, MN, USA, he joined Georgia Tech, Atlanta, GA, USA, and now is a Professor at the School of Mathematics. His research interests are in nonlinear algebra with a view towards algorithms and applications. This includes theory development, implementation of resulting algorithms in the computer algebra system Macaulay2, as well as applications to other areas of math, computer science, and engineering.
Damiano Testa studied mathematics at Università La Sapienza in Rome, Italy as an undergraduate and at MIT as a graduate student. After postdoctoral appointments at Cornell University, La Sapienza, Jacobs University Bremen and Oxford University, he joined the faculty at University of Warwick in the mathematics department. His research interests revolve around algebraic geometry, number theory and formalization of mathematics. He is also one of the maintainers of Mathlib, the main mathematics library of the Lean theorem prover.
Michael Stillman studied mathematics at University of Illinois as an undergraduate and at Harvard as a graduate student. After postdoctoral appointments at University of Chicago, Brandeis, and MIT, he joined the faculty at Cornell University in the mathematics department. His research interests revolve around computational algebraic geometry, including algorithms, implementations, and applications (to e.g. biology and theoretical physics). He is one of the creators of the Macaulay2 computer algebra system.