Talking about the finite group classification, there was a project which achieved to formally prove it correct in Coq for the odd case: http://www.msr-inria.fr/

Talking about the finite group classification, there was a project which achieved to formally prove it correct in Coq for the odd case: http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/ http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/ However, having a Coq proof does not mean someone human understand the proof, and the software can evolve in incompatible versions unable to recheck the proof.