7
$\begingroup$

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?

|cite|improve this question
$\endgroup$
  • 2
    $\begingroup$ 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". $\endgroup$ – Max Jul 21 '17 at 22:15
  • 3
    $\begingroup$ 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. $\endgroup$ – Daniel Schepler Jul 21 '17 at 22:15
  • $\begingroup$ 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 $\endgroup$ – reuns Jul 21 '17 at 23:01
  • 1
    $\begingroup$ @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. $\endgroup$ – tparker Jul 21 '17 at 23:11
4
$\begingroup$

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.

|cite|improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.