> And rigor itself? A relatively modern requirement. Perhaps. I would argue that it is LONG overdue. > Moreover, math itself resists rigor in a fundamental w

> And rigor itself? A relatively modern requirement. Perhaps. I would argue that it is LONG overdue. > Moreover, math itself resists rigor in a fundamental way, as Godel showed us. This merely shows that some things cannot be proved, be it by machine or computer. That's not the issue. The issue is whether or not we should be moving towards machine-verified proofs, since "proofs" verified only by humans often turn out to be wrong. > Machine proofs? Eh. Ultimately, everything is up to humans, even the axioms. Will the computer believe in the axiom of choice? A computer will "believe" the axiom of choice if it is told that it is an axiom. I agree that the humans get to decide what is an axiom (at least in their system), but it should be immediately obvious exactly what axioms are being accepted, and then rigorously shown that only those accepted axioms are being used. I can even point to a demonstration. One of the mathematical formalization tools available today is Metamath ( http://us.metamath.org/ http://us.metamath.org/ ). In Metamath you can state the axioms you wish to accept, and then generate proofs that are automatically checked; every step must lead back to a previously-proved theorem or an axiom. There are several existing Metamath databases. The "set.mm" database (Metamath Proof Explorer) is based on classical logic, ZFC, and the axiom of choice. Since the axiom of choice is included as an axiom, you can use it. See here: http://us.metamath.org/mpeuni/mmset.html http://us.metamath.org/mpeuni/mmset.html In contrast, the "iset.mm" database (Intuitionistic Logic Explorer) is based on intuitionistic logic and does not include the axiom of choice. Since the axiom of choice is not included, you cannot verify a proof that tries to use it - the verifier will simply complain that the step is invalid if you try to do it. See here: http://us.metamath.org/ileuni/mmil.html http://us.metamath.org/ileuni/mmil.html