Sorry I wasn't clear, but Godel's theorems have not made the formalization (in the sense of writing machine-checkable, or at least fully explicit proofs) imposs

Sorry I wasn't clear, but Godel's theorems have not made the formalization (in the sense of writing machine-checkable, or at least fully explicit proofs) impossible or undesirable. The reason we don't write up the proofs in mathematical papers as Coq files or something equivalent is purely practical: doing so for most mathematics is exceedingly tedious with our existing tools. In addition, proof assistants have a steep learning curve even for mathematicians, as they are designed by mathematical logicians who have a very specific kind of mathematics in mind. What these theorems made hopeless is the formalization of the concept of "the" natural numbers. Previously, it was taken for granted that our definitions of the natural numbers entirely fixed the truth of all of the statements you could make about them. However Godel showed that we have to pick a particular formalization, which will necessarily leave some facts about the natural numbers undetermined. Even simple theories which formalize the natural numbers and nothing else (e.g. Peano arithmetic) suffer from this problem. This results in things like non-standard arithmetic[1], which no axiomatization of the natural numbers can possibly avoid entirely. Most of mathematics is not about the natural numbers directly, but virtually all mathematical structures can be used to model the natural numbers with addition and multiplication in some way (e.g. Dimensionality of vector spaces) so similar restrictions apply here too. But none of this gives us any reason to avoid formal proofs; if a mathematician feels that an informal proof truly omits an important step or is missing full justification of a statement then they would regard the proof as incomplete (at least until the issue is clarified). [1]: https://en.m.wikipedia.org/wiki/Non-standard_model_of_arithmetic https://en.m.wikipedia.org/wiki/Non-standard_model_of_arithm...