What is the reason we usually don't use formal proofs in mathematics?

Question

Is the reason for not using formal proofs very often in mathematics because it is usually too lengthy for a person to make such a proofs or the reason is that it is simply not possible for everything in math to be formally proved?

Answer 1

tl;dr There is little reason to make paper-and-pencil formal proofs other than learning about formal logic. Machine-checked proofs take less effort to produce and are more valuable than paper-and-pencil formal proofs. Machine-checked formal proofs do take more effort to produce than informal proofs, though the extent is dramatically overblown. Currently, most mathematicians seem unaware of and/or misinformed about the capabilities of modern proof assistants. Regardless, the incentives are currently strongly aligned against a working mathematician producing machine-checked proofs, though that is starting to change. Basically, there is virtually no demand for or reputational advantage for the author to produce a machine-checked proof as opposed to an informal one, e.g. it won't increase the chance your paper gets published typically, and there is virtually no cost (reputational or otherwise) for the author of producing incorrect proofs or even incorrect theorems. I think both of these will change in the near-ish future. In particular, I think software engineering will start to significantly demand machine-checked proofs and there will be very clear financial incentives.

---

The reasons are pretty much entirely social at this point, though some of the issues aren't easy to eliminate.

The issue splits into two parts: expressing theorems and proofs in a formal system (e.g. FOL+ZFC) for "paper and pencil" proofs, and expressing theorems and proofs in a machine-checkable manner.

For the former, there are a variety of practical difficulties that make it cumbersome and there's just very little pay-off for doing it. The experience using machine-checked systems is one of the system constantly pointing out the mistakes you made. Without that, you are basically guaranteed to make errors unless you invest a huge amount of effort in checking your work. Also, one of the benefits of formalization is to have a clear chain of truth back to the axioms, but without a library of formal proofs in the same system you are using, you have to recreate everything from scratch every time you want to prove something formally most of which will be uncontroversial and irrelevant to your point. You can mitigate this by just assuming various theorems but then you lose the chain of truth.

The bigger issues is that there is basically no social benefit to doing this, and the improvement in clarity you might gain is probably not worth the effort. Socially speaking, there is virtually no demand for formal proofs from other mathematicians and its clearly unnecessary to publish a paper. In fact, I would go further and suggest that mathematical community discourages formal proofs. A paper-and-pencil formal proof is not particularly reusable, so the main output of a paper containing one is likely just that the theorems are true which an informal proof accomplishes almost as well. Formal proofs can also make it harder to see the main ideas of the proof, which can make them even less desirable than informal proofs. There's also very little reputational penalty for publishing broken proofs or even false theorems. Egregious errors will be caught before a (peer-reviewed) paper is published, so any errors that survive the peer-review process are inherently ones that are easy to miss. This means many future readers won't notice these errors, and once the errors are discovered the community will be pretty forgiving of the original author. There are some other issues but many of them are shared with machine-checked systems.

Proof assistants such as Coq, Mizar, or Isabelle/HOL resolve many of the issues with paper-and-pencil formal proofs. The most notable part is they dramatically reduce the cost of checking a formal proof and of producing one in the first place. The first social issue here is it seems the vast majority of mathematicians have little knowledge (or maybe even awareness) of proof assistants. In fact, this also applies to paper-and-pencil formal proofs: most mathematicians would need to do a good amount of study before they could write a simple but non-trivial formal proof with any confidence. There is also, currently, a rather steep learning curve for these things meaning you have to have a decent amount of motivation to stick with it. This means that there is little social support within the mathematics community for learning these things. You are very unlikely to take a course on using Coq, say, as a math major or even have such a course available (unless it's under the CS division).

At a bit more technical level, Coq, Mizar, and Isabelle/HOL use three very different foundations. Coq is based on intuitionistic type theory and a propositions-as-types view of proving things. Mizar is based on Tarski-Grothendieck set theory and is the foundation closest to what is traditionally taken as foundations. Isabelle/HOL is based on classical higher-order logic which is presented as a (non-dependently typed) type theory. Even systems that have roughly the same foundations as Coq, such as Agda and LEAN, they are not at all compatible. This leads to fragmentation and duplicated effort. It also makes it unclear which system you should learn and use. Assuming this plays out similarly to programming languages, this is not going to change, but there will and are already some "winners" which have substantially more support.

Once you have decided on a proof assistant to use, there's not much guidance on how this interfaces with traditional publishing of papers. It's only recently that some journals have started to try to establish a process for accepting (machine-checked) formalized mathematics. This would, of course, still be only for new or notable results. If your contribution is instead just formalizing some existing mathematics, this will probably not lead to a publication in a journal that is very relevant to mathematicians. Even for new results, the addition of a machine-checked proof will probably not have much relevance to most mathematicians unless the result is one with a history of incorrect proofs or is extremely surprising. (For example, Edward Nelson was trying to show that PA is inconsistent, a result no one would believe without a machine-checked proof which Nelson understood.)

This ends the answer to your question of why formal proofs aren't used. To explicitly address theorems that can't be formally proven, as stated in the comments, this is almost never an issue for most mathematicians. Even when it comes up, the meta-theorems are themselves formalizable. For example, not only is Gödel's incompleteness theorem formalizable, but it has been formalized in Coq. A proof that some theorem is undecidable in theory $T$ is just a proof in another theory $T'$ that is (usually) stronger than $T$. In the best case, you can just prove your undecidable statement implies some other statement that is already known to be undecidable in the relevant system. In the worst case, you need to model your system within your system (which is readily done for any suitable foundations, e.g. ZFC can easily model FOL proofs and semantics and then the ZFC first-order theory). Of course, the proof of undecidability will be conditional on some unprovable statement representing the stronger theory.

From this point on, I'm going to say why you (maybe) should learn and produce (machine-checked) formal proofs. I'll use "formal proof" to refer to specifically machine-checked proofs from now on. First, formal proofs (even paper-and-pencil ones) can often reveal insights. To quote Gonthier on the formal proof of the four color theorem (in Coq):

[W]e were pleasantly surprised to uncover new and rather elegant nuggets of mathematics in the process. In hindsight this might have been expected: to produce a formal proof one must make explicit every single logical step of a proof; this both provides new insight in the structure of the proof, and forces one to use this insight to discover every possible symmetry, simplification, and generalization, if only to cope with the sheer amount of imposed detail.

This is unlikely to be that compelling to most, and, frankly, is likely not enough of a benefit on its own compared to the cost. More significantly, a lot of the benefits that don't accrue to paper-and-pencil formal (or informal) proofs, do for machine-checked formal proofs. We can (and have) built libraries of formal proofs. Checking a formal proof is automated. In the comments Blue states that mathematicians "don't have that kind of time on [their] hands" to write formal proofs, but they are spending that time instead on peer reviewing correctness and, occasionally, on results or proof techniques that rely on erroneous theorems. I don't want to suggest that the amount of time spent on peer review is more than the amount of time it would take the author to formalize their proofs, especially in the current state of mechanized theorem proving. However, I do want to point out that informality has real costs too. I also don't want to completely suggest that peer review is unnecessary for formalized results. It takes someone to verify that the formal theorem statement actually corresponds to the informal theorem, e.g. the four color theorem. That said, if the theorem statement was given formally in the first place this would become unnecessary...

I don't expect a grassroots change to occur in the mathematics community to move towards formal proofs. Instead, I believe external pressures will come to bear. In particular, demand for formal proofs from the software engineering world has already started to create Proof Engineering jobs. This will be a natural career choice for a math major and will create pressure on the mathematics curriculum to support this role. In parallel, tooling, educational materials, and, particularly, library support will continue to improve so that it becomes ever more feasible to produce formal proofs. Right now, for formal proof projects the effort spent on proving the desired theorem is dwarfed by the effort to lay the groundwork for the theorems, e.g. in building up basic results. There are also clear didactic benefits to using formal proofs. Students being able to immediately tell whether their proofs are correct is a significant benefit on its own.

As a final statement, I strongly recommend reading these slides about Univalent Foundations by Vladimir Voevodsky. Many of the points I brought up are mentioned in it. I'll include a quote from those slides because of how accurately it captures the response to your question:

Among mathematicians computer proof verification was almost a forbidden subject. A conversation started about the need for computer proof assistants would invariably drift to the Goedel Incompleteness Theorem (which has nothing to do with the actual problem) or to one or two cases of verification of already existing proofs, which were used only to demonstrate how impractical the whole idea was.

To end on a more positive note though, Univalent Foundations is directly the result of a mathematician looking at doing formal proofs seriously. Becoming familiar with these systems can be rewarding on its own. Nevertheless, we are still solidly in the "early adopter" stage of this technology, so it's completely reasonable to want to wait and see how things play out.