franklin writes: <<

If a putative proof is then put into official proof format, as defined by logicians, then -- assuming sufficient computing resources -- checking it should be a piece of cake. (Each statement in sequence must be either

1) an axiom or

2) a statement B such that statements A, and A => B, are prior statements in the proof,

and the last statement is what was to be proved.)

Do you have any idea how far published mathematical proofs are from this level? I would guess that a typical published proof would require millions or even billions of statements.

...

Well, after being a mathematician for 34 years, I believe I do. Well, I believe I mentioned the hardest parts to such a project in the part of my post that you didn't quote. Obviously, if the proof being checked uses another theorem, then that theorem would have to have a seal of approval, itself. And once any theorem has been rigorously checked, and perhaps re-checked to be on the safe side, it could be adoped as an "axiom" forever after in this scheme. At first, a very large number of well-accepted and time-tested theorems would be grandfathered in -- as temporary axioms. Eventually, perhaps such a project would get around to fully checking old theorems as well.

...

So any such project would have to operate at a higher level than that. And now you come to another problem: groundbreaking results, and a large fraction of those that aren't groundbreaking, involve the introduction of one or more new ideas. And those ideas would have to be introduced to the proof machinery before it could verify the result - at which point the utility of the exercise is very much in question.

...

--Dan