The Feit-Thompson Theorem という有限群に関する定理で、元の証明が255ページもあるのを、6年かけてCoqで証明したとか。 なんという根性……  http://processalgebra.blogspot.com/2012/10/the-feit-thompson-theorem-checked-in-coq.html