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?
 A: I suspect that the reason you see more discrete math theorems formalized is just that they're "closer to the ground" than some arguments in other fields, and computer science and discrete math have been historically related, so more effort might be put in in those cases.
I don't think there's reason to believe that there is a correct "proved" result that's established enough to be in a textbook that can't be converted to a computer-checkable proof given enough time, but some proofs/methods of arguing about proofs don't lend themselves to formal arguments. 
As you point out, some of the arguments used in algebraic topology or differential geometry might involve arguing about manipulations of certain shapes based on the spatial reasoning and intuition of the reader. There are many intuitive results that would take a lot of time to formalize.

For some of the specifics you mention, someone who is not working in logic/model theory/set theory basically doesn't have to worry about second-order anything, since everything you would want can be done with the first order theory of ZFC. For example, here is a computer-checked proof that a construction of the reals is complete, based on the necessary parts of ZF. And a bit of algebraic topology has been done, like establishing the fundamental group.
