Matthew R. Ballard

Professor of Mathematics at USC.
Associate Director for Scientific Activities at ICARM.
Maintainer of Mathlib.
Fellow of the American Mathematical Society.

I am interested categorical structures, particular those arising from mirror symmetry, and in formal verification, especially of modern mathematics.

For more information about me, see my CV. For a list of my papers, please view the publications page.

Since July 2025, I have been the Associate Director for Scientific Activities at the new NSF MSRI Institute for Computer-Aided Reasoning in Mathematics, where I help to advance mathematics and the mathematical community through the use of all faces of artificial intelligence.

I am a member of the maintainer group for Mathlib, the expansive library of mathematics formalized in the Lean programming language. I always welcome a chat about how formalization, particularly Lean, can make your life better in the age of AI.

For a little of my pedagogical philosophy and experience, see my teaching page. As an extension of teaching, I take pride in mentoring researchers at all stages.

news

Sep 17, 2025 AI for Math - Bridging proof and computation
Aug 4, 2025 Institute for Computer-Aided Reasoning in Mathematics (ICARM)
Jul 23, 2025 FRG on multigraded commutative algebra, toric varieties, and mirror symmetry
Nov 1, 2024 Fellow of the American Mathematical Society
Jan 23, 2024 Research Professor at SLMath (formerly MSRI)

funding

Currently, my research is partially supported by the National Science Foundation grants DMS-2302263 and DMS-2412040, and the Renaissance Philanthropy and XTX Markets AI for Math Fund. The work has also benefited from a membership at the Institute for Advanced Study, a Research Professsorship at the Simons-Laufer Mathematical Sciences Institute (formerly MSRI), and past funding from the NSF, the Simons Foundation, USC, and the Southeastern Conference.

selected publications

  1. LNAI
    Growing Mathlib: maintenance of a large scale mathematical library
    Ballard, Matthew Robert, Baanen, Anne, Commelin, Johan, Chen, Bryan Gin-ge, Rothgang, Michael, and Testa, Damiano
    In Lecture Notes in Artificial Intelligence 2025
  2. arXiv
    King’s Conjecture and Birational Geometry
    Ballard, Matthew R., Berkesch, Christine, Brown, Michael K., Cranton Heller, Lauren, Erman, Daniel, Favero, David, Ganatra, Sheel, Hanlon, Andrew, and Huang, Jesse
    2025
  3. Crelle
    Variation of geometric invariant theory quotients and derived categories
    Ballard, Matthew, Favero, David, and Katzarkov, Ludmil
    J. Reine Angew. Math. 2019
  4. Pub. IHES
    A category of kernels for equivariant factorizations and its implications for Hodge theory
    Ballard, Matthew, Favero, David, and Katzarkov, Ludmil
    Publ. Math. Inst. Hautes Études Sci. 2014
  5. Invent. Math.
    Orlov spectra: bounds and gaps
    Ballard, Matthew, Favero, David, and Katzarkov, Ludmil
    Invent. Math. 2012