Does anyone know the status of the effort to formalise the proof of the classification of finite simple groups? Gonthier doesn't seem to have published anything about it since formalising the Odd-Order Theorem in 2013.