From Hilbert’s problem about the possibility to have an algorithm which produces a proof via the theorem of completeness of Gödel, we have an approach of automatic proof verification. In this way , we don’t try to find a new proof but only to verify a formal one. As statements of a formal theory are written in a symbolic form, if we have a finite set of axioms, we can prove in a mechanical way, that they are valid. In fact, this approach is not only theoretical and it can be formalized and implemented in a software. By this way, we have a proof assistant. A nice example is Coq which is designed to develop mathematical proofs and especially to write formal specifications, programs and proofs. Coq implements a mathematical higher -level language called Gallina. Coq provides also interactive proof methods, decisions and semi-decision algorithms, and a tactic language for letting the user define its own proof methods. It can be connected with an external computer algebra system. Even if it is rather difficult to formalize and produce mathematics, rich enough to get an automatic proof verification, Coq was able to help for this formal proof of the four color Theorem in 2005. This Theorem has been proved by Appel and Haken in 1976 with the help of a computer.. Even with the substantial modifications of Robertson, Saunders, Seymour and Thomas, the proof still used a computer code with its textual argument. But with Coq the verification was done for all. In 2012, the formal proof of Feit–Thompson Theorem was completed using Coq. This statement in Coq is:

Theorem Feit–Thompson n (gT : fin Group Type) (G : {group gT}) : odd #|G| -> solvable G.