[thoran]

It's my fault, I think I read your answer too quickly and miss a negation somewhere.

So, yes, a formal rewriting of Wiles' proof is "only" a practical challenge. But a big one. Just about 15 years ago, we were just able to prove the Fundamental theorem of algebra in Coq (a 200 years old theorem that is routinely taught to undergraduates).

[ngrilly]

That's okay @thoran! Thanks a lot for having helped me gaining a better understanding of this topic.