> for proofs of finite length in general, not just some fixed finite length.
For a brute force proof finder, for your program to be guaranteed to finish in theory, you have to pick a length. So it is fixed. Ofc you can choose whatever length you want. But you don't have that constraint with the halting oracle. Perhaps we're saying the same thing?
For the program to be guaranteed to finish in theory, all that is required is that a valid proof exists. You don't have to pick a length in advance - the program just has to keep trying proofs of progressively longer lengths.
But it won't finish if there is no proof! A halting oracle will finish either way.
Sure, but neither bcrypt or chess fall into the category of being unprovable, so having a halting detector doesn't help for those situations. The author is mixing up problems that are "hard" in the sense that we know in principle how to solve it but need a lot of resources, versus "hard" in the sense that we genuinely don't know how to solve the problem, even if we had access to infinite resources.
Mixing these two up is very misleading and detracts from what is otherwise a well written article.
This is a fair point, and I conceded it above in one of my first replies.