As part of a collaboration with Anton Leykin, Mike Stillman, and Damiano Testa, Matthew Ballard has been awarded an AI for Math grant for the project “Bridging proof and computation”.

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.