@valleyforge That makes no sense, axiom do not require proofs, they are simply chosen. Godel proved that for any chosen of axioms (of sufficient complexity) there is no machine (mechanical process) that can prove/disprove all possible theorems. There might be a mechanical process that can prove a finite set of useful theorems however, and we might be able to continually expand this finite set by choosing new axioms. The result is equivalent to Turing's on the halting problem. The opposing ambition was the god machine, whether they realized it at the time or not.