Gene wrote re proof-checking software: << Such a computer program would be as intricate as the proofs it is expected to verify, and is subject to the same human error. There cannot be certainty of correctness of a proof without certainty of the correctness of the proof-checking software. Could the program check itself?
It seems possible there could be a bootstrap method to create perfect proof-checking software (I suspect this has already been done for plane geometry), but in general this would rely on the mathematics in question having been axiomatized. Axiomatizing all of math is one of the biggest obstacles to having a universal proof-checker lies. The other is translating putative math proofs, often written largely in natural language, into putative symbolic proofs. 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.) There is also the question of the consistency of the axioms, and imo especially those of set theory/category theory. E.g., since there can't be a set of all sets, I have to question the meaning of the "class of all sets" -- a "concept" that is dubious at best. --Dan