Matthew R. Ballard

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

prof_pic.jpg

I am interested categorical structures, particularly 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

Aug 18, 2026 Palomar - a registry of Lean-verified mathematics
Jul 25, 2026 AI for Mathematics panel at ICM 2026
Jul 23, 2026 Mathematics in Lean at ICMS 2026
Jul 20, 2026 National Academies meeting on organizing mathematical knowledge
May 26, 2026 Mathlib awarded the 2026 Jean-Pierre Demailly Prize

funding

Currently, my research is partially supported by the National Science Foundation grants DMS-2302263, DMS-2412040, and DMS-2425401, 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 Professorship 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
    Matthew Robert Ballard, Anne Baanen, Johan Commelin, and 3 more authors
    In Lecture Notes in Artificial Intelligence, 2025
  2. arXiv
    King’s Conjecture and the Cox category
    Matthew R. Ballard, Christine Berkesch, Michael K. Brown, and 6 more authors
    2025
  3. Forum Sigma
    High Frobenius pushforwards generate the bounded derived category
    Matthew R. Ballard, Srikanth B. Iyengar, Pat Lank, and 2 more authors
    Forum of Mathematics, Sigma, 2026
  4. Pub. IHES
    A category of kernels for equivariant factorizations and its implications for Hodge theory
    Matthew Ballard, David Favero, and Ludmil Katzarkov
    Publ. Math. Inst. Hautes Études Sci., 2014
    DOI
  5. Invent. Math.
    Orlov spectra: bounds and gaps
    Matthew Ballard, David Favero, and Ludmil Katzarkov
    Invent. Math., 2012
    DOI