Matthew Robert Ballard

Timeline

1. 2002–2008

   Caltech and a Washington PhD

   He earns a B.S. in mathematics at Caltech in 2002. In 2008, he completes a Ph.D. at the University of Washington under Charles Francis Doran, with a dissertation on derived categories of sheaves of quasi-projective schemes.

2. 2008–2013

   Postdocs at Penn, Wisconsin and Vienna

   He is a postdoctoral researcher at the University of Pennsylvania from 2008 to 2011 and a Van Vleck Visiting Assistant Professor at the University of Wisconsin from 2011 to 2012. From 2012 to 2013, he works as a senior researcher at the University of Vienna.

3. 2013–2017

   Assistant professor and IAS member

   He joins the mathematics department of the University of South Carolina as an assistant professor in 2013. During a 2016–2017 membership at the Institute for Advanced Study in Princeton, he and collaborators develop a new method for approaching a decades-old central conjecture in his field.

4. 2018

   A Breakthrough Star award

   In 2018, he becomes an associate professor at South Carolina and is named one of the university's Breakthrough Stars, an award for early-career faculty. Richard Thomas of Imperial College credits him and his collaborators with a line of attack on the Bondal–Orlov conjecture, which no one had found a way to approach for over 20 years.

5. 2020–2023

   Joining the Mathlib maintainers

   He takes up the formalization of mathematics in 2020 as one of his pandemic projects and becomes a full professor at South Carolina in 2022. In September 2023, he accepts an invitation to join the maintainers of Mathlib, the library of formalized mathematics written in the Lean programming language.

6. 2024

   SLMath and an AMS fellowship

   He spends the Spring 2024 semester as a Research Professor at the Simons-Laufer Mathematical Sciences Institute in Berkeley, in its program on noncommutative algebraic geometry. In November 2024, the American Mathematical Society names him a Fellow.

7. 2025

   Mathlib board and Macaulay2 grant

   In June 2025, he joins the Strategic Advisory Board of the Mathlib Initiative, which supports the long-term development of Mathlib. With Anne Baanen, Johan Commelin and three other coauthors, he writes "Growing Mathlib," a 2025 paper on strategies to manage the library's growth while avoiding maintainer overload. In September 2025, he, Anton Leykin, Mike Stillman and Damiano Testa receive an AI for Math grant to build a native Lean–Macaulay2 interface that lets Lean users call Macaulay2 functions and Macaulay2 users generate Lean proofs.

8. Since July 2025

   Associate director at ICARM

   In July 2025, he becomes the founding Associate Director for Scientific Activities at the Institute for Computer-Aided Reasoning in Mathematics (ICARM), a new NSF- and Simons Foundation-funded institute at Carnegie Mellon that brings AI, formal methods and automated reasoning to mathematical research. In July 2026, he sits on AI and formalization panels at a National Academies meeting in Washington, D.C., and at the International Congress of Mathematicians in Philadelphia; in August 2026, he becomes one of four initial technical maintainers of Palomar, a public registry of Lean-verified mathematics. He remains a professor of mathematics at South Carolina and a Mathlib maintainer.