Dr. Ballard accepted an invitation to join the maintainers of Mathlib, the library of formalized mathematics written in the Lean programming language.

He is excited to be a part of the the effort.