Of course proofs can be still correct, it's just that we cannot cope with infinites very well without talking about computational limits.
My argument was hyperbolic, I regret, but it was less about what's incorrect and more about what's incomplete. The aspirations of early mathematicians was to discover a platonic ideal. Instead of that we only got useful tools that are always* up for re-interpretation depending on context.
An example of this is that Euclid's fifth postulate, which be consistent with many other interpretations of geometry too, not just the single one originally intended. It turned into a tool of formal scaffolding instead of an omnipotent "truth". Going from absolute to relative in power.
*In cases where they involve infinites. Including simple expressions like "take N to be an integer"
The predicate Halt<aType>[anExpression] is true if and only
if anExpression of type aType halts.
The predicate Halt is inferentially undecidable, that is, it
is not the case that for every expression anExpression of type aType that
|- Halt<aType>[anExpression] or |- ~Halt<aType>[anExpression].
Inferential undecidability does not mean that mathematics
is wrong.
Of course, it is possible to have incorrect
mathematical proofs, such as the incorrect proof in
[Gödel 1931] for the inferential undecidability of Russell's
Principia Mathematica. (There is a correct proof here:
https://papers.ssrn.com/abstract=3603021)