People didn't give up on ZFC because of Godel's theorem. There's currently 42 or 43 unproven 5-state Turing machines we need to confirm BB(5).
We are solving the halting problem. We are solving ZFC. That's the entire point of mathematics.
Turing's proof of the halting problem being undecidable is extraordinarily vague. It shows that for any halting procedure, there is a program (without any constraints) which violate its output. It does not, for example, rule out whether you can write a Halt procedure for no-input Turing Machines with N states. In fact we have already written them for N=1,2,3,4.
Considering Chaitin-Kolmogorov complexity, of course we can't use N bits to describe unbounded information. This doesn't in any way preclude us from making an N bit program to describe halting behavior of K<N bit programs for some N.
We are not. We're determining whether particular classes of turing machines halt, and we're determining whether particular theorems hold in ZFC (and doing a lot of mathematical work which is neither). This is not evidence that the human brain is super-turing, because these are computable problems.
> It does not, for example, rule out whether you can write a Halt procedure for no-input Turing Machines with N states. In fact we have already written them for N=1,2,3,4.
Turing didn't, but later work does. BB(748) is known to be independent of ZF. The real bound is likely much lower.
Scott Aaronson has a positive view of BB(n) being independent of ZFC. He says, we’ll need different foundations to solve k>n. And the different foundations will have their own n and etc.
Page 6 here https://www.scottaaronson.com/papers/bb.pdf