[wk_end]

That's actually a really interesting philosophical question!

Formal proofs are, of course, objects in a formal system. But as anyone who's tried to express a mathematician's proof of any real complexity in Coq can attest, they're a very small subset of the sum total of human proofs.

The proofs that mathematicians have been doing for thousands of years, by contrast, aren't formal (in the strict sense). They're arguments that appeal to the human sense of deductive reason, in a phrase. And yes, formal logic is an attempt to codify and mechanize that as an object for study, but...well, like I said, it's a big philosophical or even neurological question as to how well it does that, or can do that; to what degree that's possible.

[dwohnitmok]

While not true of thousands of years, I'm (and I think most of the mathematical community) pretty confident all of the mathematics of the last 200 can be formalized. There isn't really much of a question of whether we can formalize modern informal, rigorous proofs. Indeed a benchmark of whether a proof is rigorous or not is whether there's a clear path towards formalization (similar to how we might use as an informal benchmark whether an algorithm is well-specified by whether we have a clear path to implementing it in a real programming language).

As such mechanizing mathematics into formal proofs has yet to meet any fundamental difficulties I'm aware of. The main thing is it's just a slog and few people are working on it because it's such a slog. It can usually take orders of magnitude more time to formalize a proof than to come up with its informal, but rigorous proof. But the process doesn't really require deep insights, at least not any more than translating an algorithm from a CS textbook or paper into real code. It mainly is just because there's reams and reams of tedium that can be encapsulated in a single "mutatis mutandis" or the like.

At this point Mizar has formalized essentially all of undergraduate mathematics and is gradually working its way into graduate mathematics. It's yet to meet any deep roadblocks and it's not anticipated to meet any.

[wk_end]

Either all mathematics is formalizable and so we're not going to run into any Incompleteness Theorem-related issues and it's irrelevant...or we run into mathematics that can't be formalized and therefore mathematics isn't a fully formalizable system and so Gödel is still irrelevant :)

[dwohnitmok]

Although I understand that you mean to say Godel's Incompleteness Theorems aren't relevant, this is not because of anything related to formalization. Godel's Incompleteness Theorems don't say any particular theorem can't be formalized. All they say is that there will always be a theorem whose proof requires the assumption of an additional axiom. Very different things.

A lack of a full formalization for mathematics is more akin to a failure of Godel's Completeness Theorem (which roughly states our mathematical abstractions precisely capture the commonality between different situations we choose to abstract over). The Completeness Theorem however is proven to hold in modern mathematics (e.g. first order logic which includes ZFC).

Indeed the choice of whether to use a system fulfilling the Completeness Theorem is a conscious and true choice (unlike say Godel's incompleteness theorems whose avoidance requires giving up arithmetic), and a choice most logicians and the overwhelming majority of mathematicians decide to take. Even in higher order logics where it would appear the Completeness theorem fails, it can be recovered by appealing to a first-order understanding of its semantics. It's so much a choice that arguably you are leaving the bounds of mathematics proper and entering the wider field of philosophy if you give up the Completeness Theorem in the foundations of your mathematical system (as opposed to locally giving it up in a subsystem and analyzing it in a semantically complete metatheory).

Put another way, mathematics is precisely the study of formal objects and its standards of rigor entail that its own proofs are themselves formal objects that can be studied in their own right.

Arguing against the formalization of modern mathematics is akin to arguing that there are certain CS algorithms which cannot be turned into code. While there are certainly conceivable processes which cannot be implemented in code, algorithms in CS are essentially definitionally required to be implementable in code. Anything that is not is outside the purview of algorithms as understood by CS.

If we find a proof which essentially cannot be formalized the reaction of the mathematical community will not be to reject formalization, but rather to question the rigor of that proof. This is similar to the reaction that the computing community would have if it were to find a purported specification of an algorithm that turned out to be essentially unimplementable.