What are the limits of the modern (starting with Emil Leon Post and David Hilbert) formalization of mathematics?

Question

I've recently taken an interest in the foundation of mathematics and have read a tiny bit about various type systems, Principia Mathematica, and logic.

Personally, I'm not a big believer in the idea that mathematics can be completely formalized. I understand that mathematicians don't really do proofs completely formally for practical reasons. That make me wonder about the current status of formalized mathematics. What areas of mathematics have been completely, mechanically formalized (in the sense that there's some formal framework, and a list of formal derivations somewhere inside of that framework that formalizes such an area).

I'm not really asking for different attempts/ways at formalization, which is what's been primarily answered here What is the current state of formalized mathematics?.

Answer 1

I believe that currently accepted proofs in common mathematics such as geometry, arithmetics, algebra,... are those that we believe can be reduced to ZFC by a (very) meticulous mathematicians,thus formalizable proofs. Although, as you know formalized mathematics is only a small subset of these maths.

I see two ways to answer "yes, some math cannot be formalized.".

1. We might find some new type of (acceptable) reasoning that cannot be formalize at all. This is not even considered by any mathematician I know of. By acceptable, I mean that can be accepted as proof which is different from the way you found the proof.
2. You might want to formalize the intuition of a proof, this is a different thing and I don't think formalization is an answer to that.

Answer 2

The question as asked isn't really that meaningful. If "formalized in some way" means "logically sound and consistent", then everything that has a proof attached to it would count. There are a number of conjectures or postulates that are not proven (and so presumably wouldn't count as being "formalized" if I understand your sense of the word).

It's also interesting to note that there are the "big" conjectures (like the Riemann Hypothesis) that "everyone" knows about and knows haven't been proven, but there are so many small conjectures that either haven't been proven because no one has got to them yet, or are actually really tough problems but aren't widely known outside of small fields.

In terms of "difficult to formalize", I think that depends strongly on the problem, the mathematicians, and the techniques available. Think of the proof of Fermat's Last Theorem - this was fiendishly difficult to find and required the development of deep mathematics whose applications are much bigger than just that one theorem. In that sense, the proof of Fermat's theorem was "difficult". In another, though, it was "easy" once the appropriate mathematics were developed. It could have just been that Fermat's theorem was difficult because it was like trying to run before you can walk.

If what you mean is "for which mathematical statements are there known proofs" then the question is far too broad to answer. Keep in mind as well that mathematics isn't just "formalizations". There are also sets of methods and techniques to consider, some of which are beyond the scope of mathematics and might be considered instead to be some branch of logic.

Answer 3

Here is a table from the paper "Formal Proof" by Thomas Hales, Notices of the AMS 55(11), December 2008. It lists particular theorems, the year they were formalized, the formal theorem verifier used, the person responsible for the formal verification, and the person responsible for the original proof.

Here, as usual, "formalized" means that a proof sketch was developed which a theorem assistant was able to convert into a completely formalized proof, and then verify the formalized proof. I think it makes more sense to look at particular theorems, rather than "areas" of mathematics. Of course, to formalize a nontrivial theorem requires formalizing some amount of mathematics in the area of the theorem.

Year Theorem                     Proof System  Formalizer      Traditional Proof
1986 First Incompleteness        Boyer-Moore   Shankar         Gödel
1990 Quadratic Reciprocity       Boyer-Moore   Russinoff       Eisenstein
1996 Fundamental - of Calculus   HOL Light     Harrison        Henstock
2000 Fundamental - of Algebra    Mizar         Milewski        Brynski
2000 Fundamental - of Algebra    Coq           Geuvers et al.  Kneser
2004 Four-Color                  Coq           Gonthier        Robertson et al.
2004 Prime Number                Isabelle      Avigad et al.   Selberg-Erdös
2005 Jordan Curve                HOL Light     Hales           Thomassen
2005 Brouwer Fixed Point         HOL Light     Harrison        Kuhn
2006 Flyspeck I                  Isabelle      Bauer-Nipkow    Hales
2007 Cauchy Residue              HOL Light     Harrison        classical
2008 Prime Number                HOL Light     Harrison        analytic proof

Additional results after Hales' paper include the following (please feel welcome to update the list with significant theorems that have been formalized). Here another review https://hal.inria.fr/hal-00806920

Year Theorem                     Proof System  Formalizer     
2012 Feit-Thompson               Coq           Gonthier 
2017 Lax-Milgram                 Coq           Boldo & al