The speaker used Roc, a dependent-type-theory-based proof assistant, to formalize the Feit–Thompson theorem.

“Uh, and that is in a proof assistant known as Roc. Uh, and Roc is based on dependent type theory. Um, uh, before that I had worked with Isabelle extensively, which is a proof assistant based on, uh, on a simpler logical framework called simple type theory.”