# Why is automated proof checking so hard?

(Warn: this is not about automated proving which is impossible. It is about the automatized proof checking).

For example, there is no automated test developed for Wiles Theorem (aka Fermat last theorem) until now.

Why? My naive intuition were that it can't be much harder as the latex-formatted proof in a publication.