You don't need to implement a diagonalisation in order to prove results about it - this is true for computers as much as it is true for humans. There are formalisations of Godel's theorems in Lean, for instance. Similarly for arguments involving excluded middle and other non-constructive axioms.
I hear your point that humans reason with heuristics that are "outside" of the underlying formal system, but I don't know of a single case where the resulting theorem could not be formalised in some way (after all, this is why ZFC+ was such a big deal foundationally). Similarly, an AI will have its own set of learned heuristics that lead it to more rigorous results.
Also agree about minds and computers and such, but personally I don't think it has much bearing on what computers are capable of mathematically.
Anyway, cheers. Doesn't sound like we disagree about much.
