# Which subfields of math are easier or harder to formalize?

This is a follow-up question to Can all math results be formalized and checked by a computer?. Hopefully it's not too broad, but here goes: which subfields of math could be formalized using existing techniques, given infinite time and resources? (By "formalize," I mean "reduce proofs of all known results to abstract string manipulations using rules that are well-specified enough that the manipulations' validity could be checked by a Turing machine.") Obviously there are many well-accepted but nontrivial results whose proof's formalization would be completely infeasible in one lifetime. But are there any fields which we really have no idea how to go about formalizing?

The reason I ask is that one usually sees formalization discussed in the context of discrete math, like number theory. Carl Mummert's answer to the linked question says "Recent developments include completely verified proofs of the Prime Number Theorem (two independent formalizations), the Jordan Curve Theorem, and the Four Color Theorem," and the prime number and four-color theorems naturally fall under discrete mathematics (especially the four-color theorem - the prime-number theorem involves asymptotics, so is perhaps a bit trickier). I get the vague sense that more "continuous" branches of math, like complex analysis, differential geometry, and topology, are more difficult to formalize. (For one thing, if I understand correctly, some statements in number theory only require first-order logic and some require second-order logic, but even rigorously defining the real numbers - let alone proving theorems about them - already requires second-order logic.) Am I correct?

• Doing it all in ZFC allows to do everything in first order. As for the beginning of your question, I am no expert, but I remember seeing something along the lines of : a valid proof is a proof that one knows how to formalize, if given enough time and energy. If this is correct then this makes the question "trivial". Jul 21, 2017 at 22:15
• For what it's worth, I've seen plenty of Coq formalizations of proofs related to real analysis, general topology, measure theory, functional analysis, etc. My personal experience is that the flow of the argument is fairly straightforward and not too hard to formalize, but the details of proving real inequalities tend to bog down a bit. Jul 21, 2017 at 22:15
• The question could be : one day, all published maths results will be implemented in something equivalent to Coq, so that we are really sure the results are correct ? If so, why it isn't the case yet ? @DanielSchepler Jul 21, 2017 at 23:01
• @Max I think that definition of "valid proof" is far from accepted by all mathematicians. I've seen claims along the lines of "the large majority of mathematicians don't care whether a theorem follows logically from some set of postulates - they only care whether the theorem is true." Your proposed definition seems to lie on the anti-realist end of the spectrum of beliefs on mathematical realism. Jul 21, 2017 at 23:11