The speaker defined the complex numbers in Mathlib, proved basic results about them, and submitted the contribution as a pull request.

“And, uh, one of the things we teach them is how to define the complex numbers, which are this basic number system that goes back to Descartes. So I kind of thought, "Oh, this thing doesn't have the complex numbers.”

“Let's teach it the complex numbers." So there we go. We define the complex numbers, prove basic things about it, and it was great. And I made a pull request.”