People bringing up GIT (Goedel's Incompleteness Theorem) don't understand that GIT is a limitation of formal logic which affects human mathematicians as much as computer-based mathematicians. Both humans and computers are forced to work with a recursively enumerable set of axioms when constructing mathematical proofs, and so therefore are bound by the same limitations.
Also, if you can check a proof, then you can certainly automatically construct a proof, merely by dove-tailing over all possible proofs and checking whether they're correct and imply the desired conjecture.
In other words, using GIT when discussing proof automation is irrelevant.
Also, if you can check a proof, then you can certainly automatically construct a proof, merely by dove-tailing over all possible proofs and checking whether they're correct and imply the desired conjecture.
In other words, using GIT when discussing proof automation is irrelevant.