A group of us formalized the proof of Huang's degree theorem in summer 2019.
The proof is now maintained in the /archive directory of mathlib,
at https://github.com/leanprover-community/mathlib/blob/master/archive/sensitivity.lean