I am not an expert, but it seems to me that you still need some kind of intuition to guide you, considering that it is impossible to define even such seemingly simple ideas like “natural number” in first-order logic.
Machine proofs are a great thing, but without interpretation, we wouldn’t know what they are actually about. Like, the machine can show that if you have axiom X, Y, Z, you can prove Q. Sure, but what do those axioms mean, and why should I care about them? (I mean, I could just generate random axioms, and let the machine find some statements that can be proved from them, but would anyone want to read that?)
I am not an expert, but it seems to me that you still need some kind of intuition to guide you, considering that it is impossible to define even such seemingly simple ideas like “natural number” in first-order logic.
Machine proofs are a great thing, but without interpretation, we wouldn’t know what they are actually about. Like, the machine can show that if you have axiom X, Y, Z, you can prove Q. Sure, but what do those axioms mean, and why should I care about them? (I mean, I could just generate random axioms, and let the machine find some statements that can be proved from them, but would anyone want to read that?)