And since, arguably, the majority of AIs capable of human-level intelligence in the real world are indeed not those that are dependent on proof systems (but are, instead, complex systems), the argument's importance diminishes to a vanishingly small level.

I must be missing something here, but you are saying that a plausible argument about a technology we don't yet have makes a statement about limits of a different form of that technology completely unimportant. It seems like there's a big jump here from "arguable" and "majority" to therefore this doesn't matter.