Didn't Gödel explicitly proof that there are some statements that cannot be proven this way? Is it just assumed that these will not be relevant for all the hard problems that humans cannot solve or am I missing something here?
1. rarely does that come up in practical problems
2. for many reasons (and completeness is one) the machine cannot prove the next version is better, thus must discard it