Mathematics in Lean at ICMS 2026

Together with Rémy Degenne and Damiano Testa, Matthew Ballard co-organized the Mathematics in Lean session at the International Congress on Mathematical Software 2026. The session brought together research in mathematical formalization using Lean with new tools and software for formal mathematics, including work on AI-assisted formalization and the formalization of current mathematical research.

Ballard was also a coauthor of the ICMS proceedings paper “A Macaulay2-Lean interface for proofs in Lean” with Anton Leykin, Michael E. Stillman, Damiano Testa, Douglas A. Torrance, and Jay Yang, work arising from the Bridging Proof and Computation project.