A proof of this theorem was also formalized in the Rocq proof assistant (called Coq back then). See here for more: https://inria.hal.science/hal-04034866/document