7
$\begingroup$

It is sometimes asserted that human-readable mathematical proofs that we construct and publish are just informal approximations to the gold standard, which is a completely formal proof in a formal language. The formal proof is supposed to be the real McCoy, the pinnacle of Platonic perfection, which our messy informal proofs try their best to gesture toward.

I seem to recall reading criticisms (of the above assertion) that focused on the enormous size of formal proofs, claiming that they were so large and unwieldy that it would be impossible to write them down in full. If they are so large that we cannot actually produce them or even properly grasp them in our minds, then can we legitimately claim that such fictions are what proofs really are, or strive to be?

Although I feel that I have encountered the above criticism many times, I am having trouble finding an explicit example of someone making this kind of argument in print. The closest thing I have found is A. R. D. Mathias's essay, A term of length 4,523,659,424,929, which discusses a system for set theory due to Bourbaki, and emphasizes the gigantic size of even very simple terms in the system. However, Mathias's criticism is narrowly focused on Bourbaki's system in particular, and he does not take the additional step of arguing that all fully formal proofs are too long to write down, and (thus) cannot in any sense be what mathematical proofs really are, or aspire to be.

In the introduction to the book 18 Unconventional Essays on the Nature of Mathematics, Reuben Hersh recalls the distinction that he made in his earlier book (What Is Mathematics, Really?) between formal proof and "an argument accepted as conclusive by the present-day mathematical community," and mentions the Flyspeck Project to produce a completely formal proof of the Kepler Conjecture. Hersh writes, "I do not know anyone who thinks either that this project can be completed, or that even if claimed to be complete it would be universally accepted as a convincing proof of Kepler's conjecture." What Hersh writes here is close to what I am looking for; on the question of what proofs really are, he clearly favors informal proof over formal proof, and he expresses some skepticism about formal proofs that is related to their size. But he still stops short of arguing that formal proofs of nontrivial mathematical theorems are simply too large and complicated to ever instantiate in the real world.

Is there a better published reference for the argument that (1) formal proofs of nontrivial theorems are intrinsically so huge that they will forever remain figments of our imagination, and (2) therefore we should be skeptical of the role of formal proofs in the justification of mathematical knowledge? I'm imagining that such a reference would likely date from the mid-20th century, since nowadays the existence of computerized proof assistants makes it much harder to argue that fully formal proofs of nontrivial theorems can never be instantiated in the real world.

Improve this question
$\endgroup$
9
  • 1
    $\begingroup$ It would very strange if somebody claimed that all formal proofs are impossible to write. (Russel and Whitehead, I think, we're doing exactly this with some formal proofs.) Maybe the claim was that it is impossible to write formal proofs of all extant mathematical results? $\endgroup$
    – Moishe Kohan
    Commented May 26, 2022 at 3:18
  • 2
    $\begingroup$ @MoisheKohan If you read carefully what I wrote, I referred to formal proofs of nontrivial theorems. Does that answer your question? $\endgroup$
    – Timothy Chow
    Commented May 26, 2022 at 3:56
  • $\begingroup$ Oh, never mind then... $\endgroup$
    – Moishe Kohan
    Commented May 26, 2022 at 4:23
  • 2
    $\begingroup$ @paulgarrett In case it's not clear, I'm trying to track the history of the debate, not engage in the debate itself. This is the HSM SE site, after all. $\endgroup$
    – Timothy Chow
    Commented May 26, 2022 at 22:21
  • 1
    $\begingroup$ @TimothyChow, yes, I do understand, but/and I do also think that some of the problems in accurate history involve accurate framing of the question. :) $\endgroup$
    – paul garrett
    Commented May 30, 2022 at 1:50

3 Answers 3

Reset to default
4
$\begingroup$

Would you be thinking of this passage in the introduction of Bourbaki's Théorie des ensembles, page I 10? (Google preview)

Si la mathématique formalisée était aussi simple que le jeu d’échecs, une fois décrit le langage formalisé que nous avons choisi, il n’y aurait plus qu’à rédiger nos demonstrations dans ce langage ... un tel projet est absolument irréalisable; la moindre demonstration du debut de la Théorie des Ensembles exigerait déjà des centaines de signes pour être complètement formalisée.

Same passage in its English translation (Google preview), boldface emphasis mine:

If formalized mathematics were as simple as the game of chess, then once our chosen formalized language had been described there would remain only the task of writing out our proofs in this language ... such a project is absolutely unrealizable : the tiniest proof at the beginning of the Theory of Sets would already require several hundreds of signs for its complete formalization.

Bourbaki goes on to claim that it is necessary to use lots of abbreviations to make the language more manageable than the formalized language, and any mathematician worth his salt will be convinced that such things can be taken as shorthand descriptions of the formal thing. And that the abbreviation rules themselves must be informal, because otherwise they will be too complicated to be useful.

It seems to me that this is meant to be a general statement against the longhand use any formal system, not just the particular one they have chosen in the book. (Literally it says "our chosen formalized language" but that might mean "whatever language we have chosen to formalize, ...").

This passage is discussed by Thomas Hales in ''Developments of formal proofs'' (arXiv 2014; see page 15: "Bourbaki objected that formal proofs are too long"). Bourbaki's words seem widely cited, e.g. "require several hundreds of signs", so that might also give some leads.

Improve this answer
$\endgroup$
4
  • 2
    $\begingroup$ Thanks for this pointer. I had taken Bourbaki to be saying only that abbreviations were necessary, but hadn't realized that they regarded abbreviations as necessarily informal. I will take a closer look at this. $\endgroup$
    – Timothy Chow
    Commented May 28, 2022 at 12:46
  • $\begingroup$ I'm looking at Bourbaki now. He does say that if we use a language with abbreviations, "we no longer have the certainty that the passage from one of these languages to the other can be made in purely mechanical fashion." And this: "formalized mathematics cannot in practice be written down in full." This is about as explicit as one could hope for, so I'm accepting this answer. $\endgroup$
    – Timothy Chow
    Commented May 31, 2022 at 15:34
  • $\begingroup$ One thing that puzzles me is how definitive they meant that statement to be ("cannot in practice be written down in full"). Is it an observation of the current state of affairs back then, or is it a statement of necessity. Of course that passage is over 50 years old. It might not have been clear if computers will make "formal abbreviations" practical. $\endgroup$
    – Jukka Kohonen
    Commented Jun 1, 2022 at 10:41
  • $\begingroup$ There is some discussion of this point on MathOverflow. Abbreviations are absolutely crucial, so a lot depends on how one views them. Bourbaki says that abbreviations cannot with "certainty" be "made in purely mechanical fashion." This to me sounds like a claim that even with computers, one is in trouble. Of course, Bourbaki may not have thought too hard about the matter since he wasn't trying to prove that full formalization of mathematics is impossible in practice. $\endgroup$
    – Timothy Chow
    Commented Jun 1, 2022 at 12:49
4
$\begingroup$

In Donald Mackenzie's article, The Automation of Proof: A Historical and Sociological Exploration, I found some statements by P. Nidditch that come close to what I have been looking for.

In the whole literature of mathematics there is not a single valid proof in the logical sense … The number of original books or papers on mathematics in the course of the last 300 years is of the order of 106; in these, the number of even close approximations to really valid proofs is of the order of 101 … In the relatively few places where a mathematician has seriously tried to give a valid proof, he has always overlooked at least some of the rules of inference and logical theorems of which he has made use and to which he has made no explicit reference.

As for whether full proofs could in principle be written down, Nidditch wrote:

Since no mathematician has ever constructed a complete proof, his reputed capacity for doing so has no better status than an occult quality.

Improve this answer
$\endgroup$
0
$\begingroup$

Do we say the presentation in Whitehead & Russell is not fully formal?

picture

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ This is potentially a long discussion, but the short version is: (1) their theorems are all pretty much trivial; (2) much of it is not in fact fully formal by modern standards, as (for example) Goedel pointed out; (3) when people checked the more formal (propositional) part of it later on with computers, they found some errors. For the present discussion, (1) is the most relevant. The main question is whether proofs of substantive theorems that research mathematicians actually care about (as opposed to "toy" theorems) can be made fully formal. $\endgroup$
    – Timothy Chow
    Commented Sep 10, 2023 at 18:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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