Feit–Thompson theorem: formal proof using Coq was completed in September 2012.
法伊特-汤普森定理：在2012年九月使用 Coq 完成正式的证明。