The most definitive version of a proof one can imagine is when the proof has been expressed via a formal language and a proof assistant checks that each step of

The most definitive version of a proof one can imagine is when the proof has been expressed via a formal language and a proof assistant checks that each step of the proof complies with axioms or already proven theorems from a library (which, in this case, are simple rewrite rules in the formal grammar). The [Mizar System](https://en.wikipedia.org/wiki/Mizar_system https://en.wikipedia.org/wiki/Mizar_system) is an example of that. The question of formally proving Wiles' theorem is [discussed here](http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html). Currently there exists no tool powerful enough to formalize such proof. It's considered a challenging problem in computer science.