Human mathematicians are bound by Gödel's theorem in exactly the same way computer software is. If an informal human-based "proof" does something that would be impossible with a formal software-based proof, then it's incorrect. There is no theoretical advantage to running the calculations on a human brain.
Sorry, I didn’t intend to suggest that running a proof on wetware had advantages. Simply that running complete, from first principal proofs were doomed to failure
