Suppose I say “Here is a machine-checked proof of Fermat’s last theorem (FLT)”. How can you use my putative machine-checked proof as evidence for belief in FLT? I start from the position that you must have some personal experience of understanding to attain belief, and to have this experience you must engage your intuition and other mental processes which are impossible to formalise.

Later in the paper, Pollack writes “I have suggested how belief in correctness of a formal proof comes from engaging our own understanding to check it (and recheck it if necessary), and from the social process of many knowledgeable readers independently checking it.” Emphasis mine; the point about the social process is important, as we are now (or soon will be) drowning in machine-produced “results”. Will the social process of checking scale to match?