> We are solving the halting problem. We are solving ZFC. That's the entire point of mathematics.

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.