According to my very fresh reading on this topic, you are right, but your comment give the impression that writing Wile's proof in a machine-checkable language

According to my very fresh reading on this topic, you are right, but your comment give the impression that writing Wile's proof in a machine-checkable language is not very different from writing it in a human language. According to this article, I understand it is a lot more difficult to write a proof in a machine-checkable language, in the current state of the art: http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html http://www.cs.rug.nl/~wim/fermat/wilesEnglish.html I read a lot of comments on Hacker News and Lobsters saying "you could have avoided this bug by writing your program in Idris, Coq, Haskell, etc. and enjoying the benefits of the Curry-Howard Isomorphism". But I'm under the impression that most of this comments undervalue the effort in "feeding" the type/proof checker with the necessary formalism. I'm not saying that establishing a proof is worthless. Of course there is a lot of value in having a formal proof. I'm just saying that even for full-time professional mathematicians, machine-checkable formal proofs are still the exception, not the norm. This suggests the cost of building these proofs is still high, and it may explain why the practice is still limited in the field of computer science.