3
$\begingroup$

(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.

$\endgroup$
3
$\begingroup$

The short answer is that almost all mathematicians do not write proofs in a sufficiently formalized manner, because they rely on the intelligence of other mathematicians who read their proofs. It is not an issue of unambiguous formatting (type-setting), but an issue of strictly enforced structure and syntax, in much the same way as a compiler will reject a program if there is just one syntax error. Mathematical proofs today are also commonly in prose format, without any indication of scoping, unlike in a typical general-purpose programming language. Also, we see many varieties of 'human' shortcuts like "WLOG" and "It suffices to consider" and "Clearly", which are often not so clear. The amount of mental effort you need to verify a proof yourself with certainty indicates how much information is missing from the proof, which a computer cannot easily supply unlike a person with mathematical training.

One currently ongoing endeavour that may be of interest to you is the Flyspeck Project, which attempts to rectify the lack of absolute confidence in the proof of Kepler's conjecture due to issues such as those mentioned above.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.