Any formal system for encoding mathematics, be it ZFC, ETCS, or type theory, must by its nature be careful about many things that mathematicians usually gloss over. Ordinary mathematical notation and writing is, technically speaking, ambiguous and full of gaps, trusting the human reader to draw “obvious” conclusions. But to give a mathematical theory of mathematics we have to remove all such ambiguity and fill in all the gaps. This causes the syntactic formulas of the formal system to appear quite verbose, and often barely comprehensible to a mathematician accustomed to informal mathematical language.
Shulman, M. (2021). Homotopy type theory: The logic of space.
In advanced mathematical literature, proofs are usually presented in the form of short outlines that often only an expert can follow. This is partly out of a desire for brevity, but it would also be unwise (even if it were practical) to present proofs in complete formal detail, since the overall picture would be lost.
A solution I envision that would allow mathematics to remain acceptable to the expert, yet increase its accessibility to non-specialists, consists of a combination of the traditional short, informal proof in print accompanied by a complete formal proof stored in a computer database. [...] In addition, the computer database would have the advantage of providing absolute assurance that the proof is correct, since each step can be verified automatically. [...]
But what, exactly, constitutes a proof? Who is to say whether a proof is correct or not? Maintaining that a proof need convince only the person reading it gives the notion a subjective character. In practice, proofs tend to become generally accepted when they persuade not just one or two people but a broad or particularly influential group of mathematicians. Yet as Hobbes himself noted, this does not entirely avoid the subjective and fallible character of the judgment [...]
Every working mathematician must routinely deal with inferential gaps, misstatements, missing hypotheses, unstated background assumptions, imprecise definitions, misapplied results, and the like. [...]
Ordinary mathematical proofs tend to emphasize, in contrast [to formal proofs], the intermediate statements and goals, often leaving the justification implicit. [...]
When it comes to informal proof, mistakes arise from gaps in the reasoning, appeal to faulty intuitions, imprecise definitions, misapplied background facts, and fiddly special cases or side conditions the author failed to check. When verifying a theorem interactively, users cannot get away with any of this; the proof checker keeps the formalizer honest, requiring every step to be spelled out in complete detail. The very process of rendering a proof suitable for machine verification requires strong discipline; even if there are lingering doubts about the trustworthiness of the proof checker, formal verification delivers a very high degree of confidence — much higher than any human referee can offer without machine assistance.
Avigad, J., & Harrison, J. (2014). Formally verified mathematics.
In 1999–2000, again at the IAS, I was giving a series of lectures, and Pierre Deligne (Professor in the School of Mathematics) was taking notes and checking every step of my arguments. Only then did I discover that the proof of a key lemma in my paper [“Cohomological Theory of Presheaves with Transfers”, written in 1992–93] contained a mistake and that the lemma, as stated, could not be salvaged. [...]
This story got me scared. Starting from 1993, multiple groups of mathematicians studied my paper at seminars and used it in their work and none of them noticed the mistake. And it clearly was not an accident. A technical argument by a trusted author, which is hard to check and looks similar to arguments known to be correct, is hardly ever checked in detail. [...]
Mathematical research currently relies on a complex system of mutual trust based on reputations. By the time [Carlos] Simpson’s [1998] paper ["Homotopy Types of Strict 3-groupoids", which claimed to provide an argument that implied that the main result of the “∞-groupoids” paper, which Michael Kapranov and I had published in 1989, cannot be true] appeared, both Kapranov and I had strong reputations. Simpson’s paper created doubts in our result, which led to it being unused by other researchers, but no one came forward and challenged us on it.
Voevodsky, V. (2014). The origins and motivations of univalent foundations. - https://www.ias.edu/ideas/
The important datum to explain isn’t that somehow ordinary mathematical proof offers an a priori certitude that surpasses our certainty of other matters: it offers nothing like this. The belief that it does is nurtured, at least in large part, by the illusion that mathematical proofs standardly take a form where we understand them as wholes, that we understand ‘in a movement of thought which is continuous and nowhere interrupted’, as Descartes once put it, [...]
Azzouni, J. (2013). The relationship of derivations in artificial languages to ordinary rigorous mathematical proof.
One difficulty often encountered by the classical mathematician when faced with learning about type theory is that it is usually presented as a fully or partially formalized deductive system. This style, which is very useful for proof-theoretic investigations, is not particularly convenient for use in applied, informal reasoning. Nor is it even familiar to most working mathematicians, [...]
The history of mathematics is full of philosophically and ethically troubling reports about bad proofs of theorems. [...]
A proof typically consists of a series of assertions, each leading more or less to the next, and concluding in the statement of the theorem. How one gets from one assertion to the next can be complicated, since there are usually gaps. We have to interpolate the missing arguments, or at least believe that a good graduate student or an expert in the field can perform the interpolation. [...]
There is nothing improper about gaps in proofs, nor is there any reason to doubt that most gaps can be filled by a competent reader, exactly as the author intends. The point is simply to emphasize that proofs have gaps and are, therefore, inherently incomplete and sometimes wrong. [...]
Perhaps we should discard the myth that mathematics is a rigorously deductive enterprise. It may be more deductive than other sciences, but hand-waving is intrinsic.
Nathanson, M. B. (2009). Desperately seeking mathematical proof.
Traditional mathematical proofs are written in a way to make them easily understood by mathematicians. Routine logical steps are omitted. An enormous amount of context is assumed on the part of the reader. Proofs, especially in topology and geometry, rely on intuitive arguments in situations where a trained mathematician would be capable of translating those intuitive arguments into a more rigorous argument.
A formal proof is a proof in which every logical inference has been checked all the way back to the fundamental axioms of mathematics. All the intermediate logical steps are supplied, without exception. No appeal is made to intuition, even if the translation from intuition to logic is routine. Thus, a formal proof is less intuitive, and yet less susceptible to logical errors.
There is a wide gulf that separates traditional proof from formal proof. For example, Bourbaki’s Theory of Sets was designed as a purely theoretical edifice that was never intended to be used in the proof of actual theorems. Indeed, Bourbaki declares that “formalized mathematics cannot in practice be written down in full” and calls such a project “absolutely unrealizable”. [...]
As the art is currently practiced, each formal proof starts with a traditional mathematical proof, which is rewritten in a greatly expanded form, where all the assumptions are made explicit and all cases are treated in full. [...] From the expanded text, a computer script is prepared, which generates all the logical inferences of the proof. The transcription of a single traditional proof into a formal proof is a major undertaking. [...]
Ultimately, the mathematical corpus is no more reliable than the processes that assure its quality. A formal proof attains a much higher level of quality control than can be achieved by “local checks” and an “examination of methods”.
Hales, T. C. (2008). Formal proof.
[...] many great and important theorems don’t actually have proofs. They have sketches of proofs, outlines of arguments, hints and intuitions that were obvious to the author (at least, at the time of writing) and that, hopefully, are understood and believed by some part of the mathematical community. [...]
Even Euclid got things wrong, in the sense that there are statements in the Elements (e.g., Book I, Proposition 1) that do not follow logically from the axioms. [...]
We (the mathematical community) believe that the proofs [Wiles’ proof of “Fermat’s Last Theorem” and Perelman’s proof of the Poincaré conjecture] are correct because a political consensus has developed in support of their correctness. [...]
We mathematicians like to talk about the “reliability” of our literature, but it is, in fact, unreliable. [...]
When I read a journal article, I often find mistakes. Whether I can fix them is irrelevant. The literature is unreliable.
Nathanson, M. B. (2008). Desperately seeking mathematical truth.
My focus here is on the informal proofs that still dominate the research literature and undoubtedly will do so for the foreseeable future. What is the basis for saying that an informal proof is valid? It cannot be that it has been checked by some familiar algorithm of formal verification or computation. Certainly some parts will often have this character, but all those informal proofs that have not been formalized, but are judged correct, must have a different basis. What is it?
The familiar and almost standard answer is an appeal to understanding, a concept notable for its psychological vagueness. [...] There are too many ways of approaching the broad ill-defined concept as used in casual remarks by mathematicians to hope to glean from them a satisfactory exact concept, one suitable in itself for mathematical analysis. In general terms the situation is the same for the concept of an informal proof. Not a subject for direct, detailed formal analysis. Only the Hilbert-style formal proofs of mathematical logic, not the working informal proofs standard in all parts of mathematics, have an appropriate mathematical representation. [...]
Now broadly what I have to say about informal proofs at the psychological level is this. First, the psychological aspect is essential, because it is a mark of an informal proof that the steps in it have formal gaps. No algorithm of proof verification has been explicitly used to cover these gaps. So the basis of accepting the gaps is the implicit psychological claim that the mathematician offering the proof as a correct one has a good "understanding" of what would be needed to fill in the gaps. [...]
Suppes, P. (2005). Psychological Nature of Verification of Informal Mathematical Proofs.
[...] proofs, despite being revered as the backbone of mathematical truth, often contribute very little to a mathematician’s understanding. [...]
So what is this idea? It’s to do with truth. I claim that although proof is what supposedly establishes the undeniable truth of a piece of mathematics, proof doesn’t actually convince mathematicians of that truth. And something else does. [...]
Mathematical fact has an elevated status over other kinds of fact. It’s revered as a very certain kind of truth in a way that makes me feel uneasy, and sometimes even fraudulent. And I don’t think it’s just me. It’s not that I don’t think the things I do are true; it’s just that I don’t think they’re true for the reasons I’m philosophically supposed to.
Mathematical truth is revered because of proof. Thanks to the notion of “proof”, we have an utterly rigorous way of knowing what is and isn’t true in mathematics. How do we show that something is true? We prove it.
Or do we?
The wonderful thing about formal mathematical proof is that it eliminates the use of intuition in an argument. And the trouble with formal mathematical proof is that it eliminates the use of intuition in an argument. That is, formal mathematical proofs may be wonderfully watertight, but they are impossible to understand. Which is why we don’t write whole formal mathematical proofs — basically they’re too hard, [...]
So what sort of proofs do we write? You might think they’re something like “a series of statements that could be turned into a formal proof”. But does anyone actually prove that this could be done? No. Actually, when we write proofs what we have to do is convince the community that it could be turned into a formal proof. It is a highly sociological process, like appearing before a jury of twelve good men-and-true. The court, ultimately, cannot actually know if the accused actually ‘did it’ but that’s not the point; the point is to convince the jury. [...]
Like verdicts in court, our ‘sociological proofs’ can turn out to be wrong — errors are regularly found in published proofs that have been generally accepted as true. So much for mathematical proof being the source of our certainty. Mathematical proof in practice is certainly fallible.
Cheng, E. (2004). Mathematics, morally.
What is a proof? The question has two answers. The right wing ("right-or-wrong", "rule-of-law") definition is that a proof is a logically correct argument that establishes the truth of a given statement. The left wing answer (fuzzy, democratic, and human centered) is that a proof is an argument that convinces a typical mathematician of the truth of a given statement.
While valid in an idealistic sense, the right wing definition of a proof has the problem that, except for trivial examples, it is not clear that anyone has ever seen such a thing. The traditional examples of correct proofs that have been presented to students for over two thousand years are the geometric arguments Euclid presents in his classic text Elements, written around 350 B.C. But as Hilbert pointed out in the late 19th century, many of those arguments are logically incorrect. Euclid made repeated use of axioms that he had not stated, without which his arguments are not logically valid.
Well, can we be sure that the post-Hilbert versions of Euclid's arguments are right wing proofs? Like most mathematicians, I would say yes. On what grounds do I make this assertion? Because those arguments convince me and have convinced all other mathematicians I know. But wait a minute, that's the left wing definition of proof, not the right wing one.
And there you have the problem. Like right wing policies, for all that it appeals to individuals who crave certitude in life, the right wing definition of mathematical proof is an unrealistic ideal that does not survive the first contact with the real world. [...]
Even in the otherwise totally idealistic (and right wing) field of mathematics, the central notion of proof turns out to be decidedly left wing the moment you put it to work. In other words, the only notion of proof that makes real sense in mathematics, and which applies to what mathematicians actually do, is the left wing notion.
Devlin, K. (2003). When is a proof?
We accuse students of the high crime of "not even knowing what a proof is." Yet we, the math teachers, don't know it either, if "know" means give a coherent, factual explanation. (Of course, we know how to "give a proof" in our own specialty.)
The trouble is, "mathematical proof" has two meanings. In practice, it's one thing. In principle, it's another. We show students what proof is in practice. We tell them what it is in principle. The two meanings aren't identical. That's O.K. But we never acknowledge the discrepancy. How can that be O.K.?
Meaning number 1, the practical meaning, is informal, imprecise. Practical mathematical proof is what we do to make each other believe our theorems. It's argument that convinces the qualified, skeptical expert. It's done in Euclid and in The International Archive Journal of Absolutely Pure Homology. But what is it, exactly? No one can say.
Meaning number 2, theoretical mathematical proof, is formal. Aristotle helped make it. So did Boole, Peirce, Frege, Russell, Hilbert, and Gödel. It's transformation of certain symbol sequences (formal sentences) according to certain rules of logic (modus ponens, etc). A sequence of steps, each a strict logical deduction, or readily expanded to a strict logical deduction. This is supposed to be a "formalization, idealization, rational reconstruction of the idea of proof" (P. Ernest, private communication).
Problem A: What does meaning number 1 have to do with meaning number 2?
Problem B: How come so few notice Problem A? Is it uninteresting? Embarrassing?
Problem C: Does it matter?
Problem C is easier than A and B. It matters, morally, psychologically, and philosophically.
When you're a student, professors and books claim to prove things. But they don't say what's meant by "prove." You have to catch on. Watch what the professor does, then do the same thing.
Then you become a professor, and pass on the same "know-how" without "knowing what" that your professor taught you.
Hersh, R. (1997). What is mathematics, really?
Now if our proofs are really to carry conviction, they must, on a full analysis, rest upon obviously true premises, and proceed to their conclusions by means of inferences which obviously preserve truth. That, at least, is the ideal to which we must aspire. No doubt such an ideal can never be fully realized, if only because the notion of what is obvious may differ from person to person or from time to time. What one mathematician, or generation of mathematicians, accepts as a proof may be rejected by another.
Mayberry, J. (1994). What is Required of a Foundation for Mathematics?. Philosophia Mathematica, 2(1), 16-35.
What is a proof? [...]
The standard of correctness and completeness necessary to get a computer program to work at all is a couple of orders of magnitude higher than the mathematical community’s standard of valid proofs. [...]
When one considers how hard it is to write a computer program even approaching the intellectual scope of a good mathematical paper, and how much greater time and effort have to be put into it to make it “almost” formally correct, it is preposterous to claim that mathematics as we practice it is anywhere near formally correct.
Our system is quite good at producing reliable theorems that can be solidly backed up. It’s just that the reliability does not primarily come from mathematicians formally checking formal arguments; it comes from mathematicians thinking carefully and critically about mathematical ideas. [...]
There are people working hard on the project of actually formalizing parts of mathematics by computer, with actual formally correct formal deductions. I think this is a very big but very worthwhile project, and I am confident that we will learn a lot from it. [...]
However, we should recognize that the humanly understandable and humanly checkable proofs that we actually do are what is most important to us, and that they are quite different from formal proofs. [...]
Mathematicians were actually very quick to accept my proof [of the geometrization conjecture for Haken manifolds], and to start quoting it and using it based on what documentation there was, based on their experience and belief in me, and based on acceptance by opinions of experts with whom I spent a lot of time communicating the proof. [...]
Thurston, W. P. (1994). On proof and progress in mathematics.
[...] Just what do we mean by a "proof"?
It seems that mathematicians - and to avoid generating too many letters of complaint, let me hasten to rephrase that as "we mathematicians" - are somewhat schizophrenic when it comes to answering this question. When pressured by the persistent student, we fall back on the logician's definition and the "translatable in principle" defense. But in practice, we work happily with what is quite clearly a socially determined notion of proof.
Mathematicians know very well the scope for dispute over this [what kind of mathematical argument counts as a proof]. For example, arguments that satisfied eighteenth century mathematicians were rejected as not constituting proofs by their nineteenth century successors such as Cauchy. [...]
Indeed, the formal notion of proof seems set to become dominant in the setting of standards for high-integrity computer systems. Most interesting in this respect, because it addresses the issue directly, is the new UK Interim Defence Standard 00-55, governing the procurement of safety critical software in defense equipment. It differentiates explicitly between "Formal Proof" and what it calls "Rigorous Argument":
A Formal Proof is a strictly well-formed sequence of logical formulae such that each one is entailed from formulae appearing earlier in the sequence or as instances of axioms of the logical theory...
A Rigorous Argument is at the level of a mathematical argument in the scientific literature that will be subjected to peer review...
Unlike DeMillo, Lipton, and Pedis, who see formal proofs as the mere "imaginary logical structure" corresponding to peer-reviewed rigorous arguments, the Ministry makes it clear that in its view formal proof is to be preferred to rigorous argument:
Creation of [formal] proofs will... consume a considerable amount of the time of skilled staff. The Standard therefore also envisages a lower level of design assurance; this level is known as a Rigorous Argument. A Rigorous Argument is not a Formal Proof and is no substitute for it...
Formal Proof and the Law Courts
What will be the consequences if other regulatory bodies follow the lead of the UK Ministry of Defence, distinguishing explicitly between formal proof and rigorous argument, and making it clear that formal proof is to be preferred? [...]
It takes a leap of imagination to envisage a courtroom in which, with large sums of money at stake, lawyers have to debate the usage of the law of the excluded middle or some other aspect of mathematical logic. Yet, a few years ago it would have seemed unimaginable that a law court might have had to weigh the virtues of formal and informal mathematical proofs, as the English High Court nearly had to do in the VIPER case. It would certainly be foolish to assume that the first legal case centering on the nature of mathematical proof will be the last.
MacKenzie, D. (1992). Computers, formal proof, and the law courts.
Research mathematicians for instance seldom scrutinize the published profs of results in detail, but are rather led by the established authority of the author, the testing of special cases and an informal evaluation whether "the methods and results fit in, seem reasonable..." (Davis & Hersh, 1986:67). It is therefore within the context of the actual practice of modern mathematical research that a more complete analysis of the various functions and roles of proof is called for. [...]
With very few exceptions, teachers of mathematics seem to believe that a proof for the mathematicians provides absolute certainty and that it is therefore the absolute authority in the establishment of the validity of a conjecture. They seem to hold the naïve view described by Davis & Hersh (1986:65) that behind each theorem in the mathematical literature there stands a sequence of logical transformations moving from hypothesis to conclusion, absolutely comprehensible, and irrefutably guaranteeing truth. However, this view is completely false. Proof is not necessarily a prerequisite for conviction - to the contrary, conviction is probably far more frequently a prerequisite for the finding of a proof (For what other, weird and obscure reasons, would we then sometimes spend months or years to prove certain conjectures, if we weren't already convinced of their truth?) [...]
Absolute certainty also does not exist in real mathematical research, and personal conviction usually depends on a combination of intuition, quasi-empirical verification and the existence of a logical (but not necessarily rigourous) proof. In fact, a very high level of conviction may sometimes be reached even in the absence of a proof. [...]
It is furthermore a commonly held view among today's mathematicians that there is no such thing as a rigourously complete proof [...] Firstly, there is the problem that no absolute standard exist for the evaluation of the logical correctness of a proof nor for its acceptance by the mathematical community as a whole. [...]
The popular formalistic idea of many present mathematics teachers that conviction is a one-to-one mapping of deductive proof should therefore be completely abandoned; conviction is not gained exclusively from proof alone nor is the only function of proof that of verification/conviction. Not only does such an approach represent intellectual dishonesty, but it also does not make sense to pupils, especially where self-evident or easily verifiable statements are concerned.
Rather than one-sidedly focusing only on proof as a means of verification, the more fundamental function of explanation should be exploited to present proof as a meaningful activity to pupils.
De Villiers, M. D. (1990). The role and function of proof in mathematics.
Mathematicians admit that their proofs can have different degrees of formal validity - and still gain the same degree of acceptance. [...]
In these more recent views [last two decades], a proof is an argument needed to validate a statement, an argument that may assume several different forms as long as it is convincing. [...]
Clearly the acceptance of a theorem by practising mathematicians is a social process which is more a function of understanding and significance than of rigorous proof. Indeed, the presence of any proof, rigorous or otherwise, is only one of several determining elements in acceptance. [...]
Perhaps the situation is best discussed in terms borrowed from Maslow's theory of social motivation [Maslow, 1970]. Understanding, significance, compatibility, reputation, and convincing argument are "positive motivators" to acceptance: it is these factors which focus the attention of practising mathematicians on a new theorem and move them to its active acceptance, lifting it above the great body of equally valid but less attractive theorems which confront them in the mathematical literature. [...]
The role of proof in the process of acceptance is similar to its role in discovery. Mathematical ideas are discovered through an act of creation in which formal logic is not directly involved. They are not derived or deduced, but developed by a process in which their significance for the existing body of mathematics and their potential for future yield are recognized by informal intuition. While a proof is considered a prerequisite for the publication of a theorem, it need be neither rigorous nor complete. Indeed the surveyability of a proof, the holistic conveyance of its ideas in a way that makes them intelligible and convincing, is of much more importance than its formal adequacy [Hanna, 1983]. Since fully adequate, step-by-step proof is in most cases impracticable, and since surveyability is lost when proofs become too long, proofs are conventionally elliptical and brief. [...]
[...] to someone who is neither fully equipped to assess significance nor able to make the intuitive judgments necessary in successfully surveying a proof, it might easily appear that the manner of presentation - with its possible implication that full rigor is the ideal form - is the core of mathematical practice. Thus competence in mathematics might readily be misperceived as synonymous with the ability to create the form, a rigorous proof.
It is only one step further, then, to assume that learning mathematics must involve training in the ability to create this form. To teach a beginning student is assumed to involve teaching the formalities of proof. Paradoxically, such an emphasis omits the crucial element. When a mathematician reads a proof, it is not the deductive scheme that commands most attention. It is, in fact, the mathematical ideas, whose relationships are illuminated by the proof in a new way, which appeal for understanding, and it is the intuitive bridging of the gaps in logic that forms the essential component of that understanding. When a mathematician evaluates an idea, it is significance that is sought, the purpose of the idea and its implications, not the formal adequacy of the logic in which it is couched.
Hanna, G. (1989). More than formal proof.
There is also an idea that the proofs that are given in books and in classrooms are totally adequate, or if they are not adequate, can be made adequate just by a little bit of cosmetology, let me say. What happens when you eavesdrop on a typical college lecture in advanced mathematics? Imagine that you have broken in in the middle of a proof. Now, ideally, since proof passes from assumption to conclusion by tiny logical chains of reasoning, you should be hearing the presentation of those small, logical transformations which are supposed to lead inexorably from assumption to conclusion. But you hear very strange things. You hear such noises as, 'it is easy to show that', or 'by an obvious generalisation' or 'by a long, but elementary computation which I leave to the reader or to the student', 'you can verify so and so'. Now, these phrases are not proof. These phrases are rhetoric in the service of proof, [...]
You can raise the objection that [...] behind all of this, there really is something which you might say is an absolute in the very Platonic sense, that watertight, inexorable list of transformations which take you from hypothesis to conclusion. But this is not the case. This is an illusion. This is a myth. It doesn't exist. It probably cannot exist. In the real world of mathematics, in my view, a paper does several things. It testifies that the author has convinced himself and his friends that certain results are true and it presents part of the evidence on which this conviction is based. My job here is not to undermine the proof process but simply to place it in a realistic way. [...] the point is that, in order to evaluate a mathematical paper, you must be part of a certain mathematical subculture. Once you are there, then you will know whether a paper has proved what it claims to prove or it has not.
Davis, P. (1986). The nature of proof.
The myth of totally rigorous, totally formalized mathematics is indeed a myth. Mathematics in real life is a form of social interaction where "proof" is a complex of the formal and the informal, of calculations and casual comments, of convincing argument and appeals to the imagination. The competent professional knows what are the crucial points of his argument - the points where his audience should focus their skepticism. Those are the points where he will take care to supply sufficient detail. The rest of the proof will be abbreviated. This is not a matter of the author's laziness. On the contrary, to make a proof too detailed would be more damaging to its readability than to make it too brief. Complete mathematical proof does not mean reduction to a computer program. Complete proof simply means proof in sufficient detail to convince the intended audience - a group of professionals with training and mode of thought comparable to that of the author. Consequently, our confidence in the correctness of our results is not absolute, nor is it fundamentally different in kind from our confidence in our judgements of the physical reality of ordinary life.
Davis, P. J., & Hersh, R. (1986). Descartes' dream: The world according to mathematics.
Almost all Mathematicians now use the convenient language of set theory to describe Mathematical structures, but very few Mathematicians can recite the axioms which found set theory, while almost none of them (except for the logicians) can specify the exact rules of logical inference. [...]
To achieve complete clarity, Mathematical statements can be formulated in a specific symbolic language. [...]
Proof in Mathematics is both a means to understand why some result holds and a way to achieve precision. As to precision, we have now stated an absolute standard of rigor: A Mathematical proof is rigorous when it is (or could be) written out in the first order predicate language L(∈) as a sequence of inferences from the axioms ZFC, each inference made according to one of the stated rules. [...] To be sure, practically no one actually bothers to write out such formal proofs. In practice, a proof is a sketch, in sufficient detail to make possible a routine translation of this sketch into a formal proof. When a proof is in doubt, its repair is usually just a partial approximation of the fully formal version. What is at hand is not the practice of absolute rigor, but a standard of absolute rigor. [...]
For the concept of rigor we make a historical claim: That rigor is absolute and here to stay. The future may see additional axioms for sets or alternatives to set theory or perhaps new more efficient ways of recording (or discovering) proofs, but the notion of a rigorous proof as a series of formal steps in accordance with prescribed rules of inference will remain.
Moreover, there are good reasons why Mathematicians do not usually present their proofs in fully formal style. It is because proofs are not only a means to certainty, but also a means to understanding. Behind each substantial formal proof there lies an idea, or perhaps several ideas. The idea, initially perhaps tenuous, explains why the result holds. The idea becomes Mathematics only when it can be formally expressed, but that expression must be so couched as to reveal the idea; it will not do to bury the idea under the formalism. [...]
Proofs serve both to convince and to explain - and they should be so presented.
MacLane, S. (1986). Mathematics: form and function.
A formal mathematical proof is a finite sequence of formulas, each element of which is either an axiom or the result of applying one of a fixed set of mechanical rules to previous formulas in the sequence. It is thus possible to write a computer program to check mechanically whether a given sequence is a formal proof. However, formal proofs are rarely used. Instead, typical proofs in journal articles, textbooks, and day-to-day mathematical communication use informal notation and leave many of the steps to the reader's imagination.
Boyer, R. S., & Moore, J. S. (1984). Proof checking the RSA public key encryption algorithm.
[...] it has always been more fun to prove a theorem than to write down the proof, [...]
Mac Lane, S. (1983). The health of mathematics.
Proofs. Only professional mathematicians learn anything from proofs. Other people learn from explanations. I'm not sure that even mathematicians learn much from proofs in fields with which they are not familiar. [...]
Boas, R. P. (1981). Can we make mathematics intelligible?
Student: Sir, what is a mathematical proof?
Ideal Mathematician: You don't know that? What year are you in?
Student: Third-year graduate.
I.M.: Incredible! A proof is what you've been watching me do at the board three times a week for three years! That's what a proof is.
Student: Sorry, sir, I should have explained. I'm in philosophy, not math. I've never taken your course.
I.M.: Oh! Well, in that case - you have taken some math, haven't you? You know the proof of the fundamental theorem of calculus - or the fundamental theorem of algebra?
Student: I've seen arguments in geometry and algebra and calculus that were called proofs. What I'm asking you for isn't examples of proof, it's a definition of proof. Otherwise, how can I tell what examples are correct?
I.M.: Well, this whole thing was cleared up by the logician Tarski, I guess, and some others, maybe Russell or Peano. Anyhow, what you do is, you write down the axioms of your theory in a formal language with a given list of symbols or alphabet. Then you write down the hypothesis of your theorem in the same symbolism. Then you show that you can transform the hypothesis step by step, using the rules of logic, till you get the conclusion. That's a proof.
Student: Really? That's amazing! I've taken elementary and advanced calculus, basic algebra, and topology, and I've never seen that done.
I.M.: Oh, of course no one ever really does it. It would take forever! You just show that you could do it, that's sufficient.
Student: But even that doesn't sound like what was done in my courses and textbooks. So mathematicians don't really do proofs, after all.
I.M.: Of course we do! If a theorem isn't proved, it's nothing.
Student: Then what is a proof? If it's this thing with a formal language and transforming formulas, nobody ever proves anything. Do you have to know all about formal languages and formal logic before you can do a mathematical proof?
I.M.: Of course not! The less you know, the better. That stuff is all abstract nonsense anyway.
Student: Then really what is a proof?
I.M.: Well, it's an argument that convinces someone who knows the subject.
Student: Someone who knows the subject? Then the definition of proof is subjective; it depends on particular persons. Before I can decide if something is a proof, I have to decide who the experts are. What does that have to do with proving things?
I.M.: No, no. There's nothing subjective about it! Everybody knows what a proof is. Just read some books, take courses from a competent mathematician, and you'll catch on.
Student: Are you sure?
I.M.: Well - it is possible that you won't, if you don't have any aptitude for it. That can happen, too.
Student: Then you decide what a proof is, and if I don't learn to decide in the same way, you decide I don't have any aptitude.
I.M.: If not me, then who?
Davis, P., & Hersh, R. (1981). The mathematical experience.
Let us heed their [De Millo, Lipton and Perlis] advice and settle for the frail, human standards of mathematicians. The ACM should require that programmers convince us of the correctness of the programs that they publish, just as mathematicians must convince one another of the correctness of their theorems.
Lamport, L. (1979). in: Comments on Social Processes and Proofs. Comm. ACM, 22, 624.
The peculiarities of the human mind make it impossible in practice to verify formal deductions, even if we agree that in principle, such a verification is the ideal form for a proof. Two circumstances act together with perilous effect: formal deductions are much longer than texts in argot, and humans are much slower at reading and comprehending such formal arguments than texts in natural languages.
A proof of a single theorem may take up five, fifteen, or even fifty pages. [...]
Hence, the absence of errors in a mathematical paper (assuming that none are discovered), as in other natural sciences, is often established indirectly: how well the results correspond to what was generally expected, the use of similar arguments in other papers, examination of small sections of the proof “under the microscope,” even the reputation of the author — in short, its reproducibility in the broadest sense of the word.
Manin, Y. I. (1977). A course in mathematical logic.
[...] in an unformalized text, one is exposed to the dangers of faulty reasoning arising from, for example, incorrect use of intuition or argument by analogy. In practice, the mathematician who wishes to satisfy himself of the perfect correctness or "rigour" of a proof or a theory hardly ever has recourse to one or another of the complete formalizations available nowadays, nor even usually to the incomplete and partial formalizations provided by algebraic and other calculi. In general he is content to bring the exposition to a point where his experience and mathematical flair tell him that translation into formal language would be no more than an exercise of patience (though doubtless a very tedious one). [...] the process of rectification, sooner or later, invariably consists in the construction of texts which come closer and closer to a formalized text until, in the general opinion of mathematicians, it would be superfluous to go any further in this direction. In other words, the correctness of a mathematical text is verified by comparing it, more or less explicitly, with the rules of a formalized language. [...]
[...] no great experience is necessary to perceive that such a project [formalized mathematics] 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. [...]
[...] formalized mathematics cannot in practice be written down in full, and therefore we must have confidence in what might be called the common sense of the mathematician [...]
We shall therefore very quickly abandon formalized mathematics [...] Sometimes we shall use ordinary language more loosely, by voluntary abuses of language, by the pure and simple omission of passages which the reader can safely be assumed to be able to restore easily for himself, and by indications which cannot be translated into formalized language and which are designed to help the reader to reconstruct the complete text. Other passages, equally untranslatable into formalized language, are introduced in order to clarify the ideas involved, if necessary by appealing to the reader's intuition; this use of the resources of rhetoric is perfectly legitimate, provided only that the possibility of formalizing the text remains unaltered.
[...] dans un texte non formalisé, on est exposé aux fautes de raisonnement que risquent d'entraîner, par exemple, l'usage abusif de l'intuition, ou le raisonnement par analogie. En fait, le mathématicien qui désire s'assurer de la parfaite correction, ou, comme on dit, de la « rigueur » d'une démonstration ou d'une théorie, ne recourt guère à l'une des formalisations complètes dont on dispose aujourd'hui, ni même le plus souvent aux formalisations partielles et incomplètes fournies par le calcul algébrique et d'autres similaires; il se contente en général d'amener l'exposé à un point où son expérience et son flair de mathématicien lui enseignent que la traduction en langage formalisé ne serait plus qu'un exercice de patience (sans doute fort pénible). [...] le redressement [des doutes que viennent à s'élever] se fait invariablement, tôt ou tard, par la rédaction de textes se rapprochant de plus en plus d'un texte formalisé, jusqu'à ce que, de l'avis général des mathématiciens, il soit devenu superflu de pousser ce travail plus loin; autrement dit, c'est par une comparaison, plus ou moins explicite, avec les règles d'un langage formalisé, que se fait l'essai de la correction d'un texte mathématique. [...] et point n'est besoin d'une longue pratique pour s'apercevoir qu'un tel projet [la mathématique formalisée] est absolument irréalisable; la moindre démonstration du début de la Théorie des Ensembles exigerait déjà des centaines de signes pour être complètement formalisée. [...] la mathématique formalisée ne peut être écrite tout entière; force est donc, en définitive, de faire confiance à ce qu'on peut appeler le sens commun du mathématicien; [...] Nous abandonnerons donc très tôt la Mathématique formalisée, [...] Souvent même on se servira du langage courant d'une manière bien plus libre encore, par des abus de langage volontaires, par l'omission pure et simple des passages qu'on présume pouvoir être restitués aisément par un lecteur tant soit peu exercé, par des indications intraduisibles en langage formalisé et destinées à faciliter cette restitution. D'autres passages également intraduisibles contiendront des commentaires destinés à rendre plus claire la marche des idées, au besoin par un appel à l'intuition du lecteur; l'emploi des ressources de la rhétorique devient dès lors légitime, pourvu que demeure inchangée la possibilité de formaliser le texte.
Bourbaki, N. (1970). Théorie des ensembles.
It would be out of place to ask whether Euclid would have been able to include in his list of postulates this or that assumption if he had wanted just as even today it would, in most cases, be futile to ask a working mathematician to specify the rules of deduction that he uses in his arguments. The chances are that the typical working mathematician would reply that he is willing to leave this task to the logicians and that, by contrast, his own intuition is sound enough to get along spontaneously.
Robinson, A. (1968). Some thoughts on the history of mathematics.
On the face of it there should be no disagreement about mathematical proof. Everybody looks enviously at the alleged unanimity of mathematicians; but in fact there is a considerable amount of controversy in mathematics. [...]
I think that mathematicians would accept this [proof of Euler's well-known theorem on simple polyhedra] as a proof, and some of them will even say that it is a beautiful one. It is certainly sweepingly convincing. But we did not prove anything in any however liberally interpreted logical sense. There are no postulates, no well-defined underlying logic, there does not seem to be any feasible way to formalize this reasoning. What we were doing was intuitively showing that the theorem was true. This is a very common way of establishing mathematical facts, as mathematicians now say. [...]
Now is this a proof? Can we give a definition of proof which would allow us to decide at least practically, in most cases, if our proof is really a proof or not? I am afraid the answer is 'no'. [...]
Lakatos, I. (1961). What does a mathematical proof prove? in: Lakatos, I. (1978). Mathematics, Science and Epistemology: Volume 2, Philosophical Papers.
Those who taught me the infinitesimal Calculus did not know the valid proofs of its fundamental theorems and tried to persuade me to accept the official sophistries as an act of faith. [...]
The mathematical teaching at Cambridge when I was an undergraduate was definitely bad. [...] The 'proofs' that were offered of mathematical theorems were an insult to the logical intelligence. Indeed, the whole subject of mathematics was presented as a set of clever tricks by which to pile up marks in the Tripos. [...]
A great deal of the argumentation that I had been told to accept was obviously fallacious, [...]
And the splendid certainty which I had always hoped to find in mathematics was lost in a bewildering maze.
Russell, B. (1959). My philosophical development.
In the whole literature of mathematics there is not a single valid proof in the logical sense. We show concretely how to make mathematics a deductive science, i.e. a science in which proofs are genuine deductions (as in contemporary Formal Logic), as against the usual informal, incomplete, intuitive arguments that pass for such. [...]
[...] every mathematicians should, as a part of his training, obtain a thorough knowledge and technical mastery of the deductive method and use it in suitable sections of his subject, so that even if he does not subsequently use it in his everyday work, he will at least realise what the demands of a valid proof are and be able in principle to construct one for each of his theorems. He will become aware of what "logical rigour" really involves, and will not, as so many contemporary mathematicians do, make in ignorance unjustified claims to it. [...]
[...] in textbooks, treatises, and lectures, nearly all the detailed derivations are omitted, he [the student] is greatly helped by being supplied with genuine proofs, for in these every relevant step has to be included and its presence explained by reference to prescribed rules of inference, axioms, definitions, and previously proved theorems. [...]
In its whole literature, from Euclid to Bourbaki inclusive, there are scarcely any proofs in the logical sense. [...] It is remarkable, in view of this, that so many mathematicians pride themselves on what they call their "logical rigour".
Let us clarify this point further. Mathematics is continually asserted to be a deductive science. Yet, with the extremely rare exceptions mentioned above, there is no piece of deduction in extant mathematics. None of the so-called proofs forms a deductive chain. They are at best outlines of proofs, not themselves proofs. Many of the necessary details are ommited; [...]
For example, Veblen and Young (Projective Geometry, Vol. 1, p. 1) say: "The starting point of any strictly logical treatment of geometry (and indeed of any branch of mathematics) must then be a set of undefined elements and relations, and a set of unproved propositions involving them; and from these all other propositions (theorems) are to be derived by the methods of formal logic" (our italics). Our complaint is that Veblen and Young, in company with so many others, after advocating that the methods of formal logic have this role to play in mathematics, have failed to make their practice conform to their proposals by the actual adoption of these methods in their work.
Again, Dieudonné, one of the leaders of the Bourbaki group, has contended that as a result of the nineteenth century discoveries - by Weierstrass, Peano, and others - that are paradoxical to the intuition, "the absolute necessity is imposed henceforth on every mathematician anxious for intellectual honesty to present his reasoning in an axiomatic form, that is, in a form in which the propositions are linked together solely by virtue of logical rules" (Revue Scientifique, 1939, 77, p. 225; our translation and the author's italics). Dieudonné's contention was originally made in 1938, a year before the first Bourbaki fascicule appeared, so one might have expected that their treatise would satisfy the requirements he expressed; for were they not "anxious for intellectual honesty"? However, in spite of their pretensions ("Le traité donne... des démonstrations complètes", Mode d'emploi ce traité, p. the 1), Bourbakian Eléments de Mathématique follows the tradition of giving informal, incomplete, intuitive arguments; possibly the skilful reader could construct valid proofs out of the materials offered him, but valid proofs are not actually to be found in the work itself, and that is the decisive point, for we are concerned with what is, not with what might be if things were very different. Certainly the definitions are more precise than in (say) Euler, [...] but the method of proof is in principle the same as in other mathematical writings. Nowhere in the Eléments are "the propositions linked together solely by virtue of logical rules". [...]
On being confronted with our demands for a logical mathematics, a critic might comment along one or more of the following lines. [...]
(ii) "The proofs that are actually given in the best texts, e.g. in Bourbaki's, are satisfactory enough. They may not be complete in all details, yet they contain enough for the competent reader to be able to convince himself, by adding as many of the details as he finds appropriate, that the statement asserted to be a theorem is indeed a theorem. Consequently the sort of proof envisaged by the logician is superfluous."
This amounts to saying that the conventional validation procedure followed by the mathematician, which he has accepted uncritically since he was at school and to which he is tied by long and familiar association, is adequate for practical purposes, these being to enable the reader to satisfy himself of the correctness of given statements. But (a) it is not rare for incorrect results to win acceptance; [...] And, more importantly, (b) a proof has to conform to theoretical rather than to practical canons if one is to be rationally justified in claiming correctness; there must be explicit reference to stated standards with respect to which validity is to be judged; else "proof" degenerates into mere persuasive argumentation, rhetorical appeals, reliance on intuitive insight, or worse. [...]
The inferential apparatus, which is just as important [as axioms and definitions] since it is the means of passing beyond the starting-points, of going from these to the theorems, is not mentioned. But for at least as good reasons as those justifying the setting up of axioms and definitions, the inferential apparatus, too, ought to be made clear. And whenever one proposes in the system that such-and-such a formula is a "logical consequence" of such-and-such formulae, one has to indicate explicitly which data acted on by which elements of the inferential apparatus justify the proposal.
(iii) "The ordinary proofs in mathematics are admittedly incomplete, but any mathematician could make them complete if he was willing to take the trouble; he is not so willing because he believes that the discovery of one interesting truth is worth a hundred pieces of fruitless logic. The driving force of mathematics is creative discovery, not logical reasoning, and the way to a genuine understanding of it is by informal arguments and explanations, not by patterns of symbolic deduction."
Since no mathematician has ever constructed a complete proof, his reputed capacity for doing so has no better status than an occult quality; there is at present not the slightest evidence available for thinking that any mathematician can really give a proper proof of any mathematical theorem, and there is a good deal of contrary evidence. 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 - understandably enough, since he has not consciously thought of them. [...]
Nidditch, P. H. (1957). Introductory formal logic of mathematics.
[...] But I discovered that many mathematical demonstrations, which my teachers expected me to accept, were full of fallacies, and that, if certainty were indeed discoverable in mathematics, it would be in a new kind of mathematics, with more solid foundations than those that had hitherto been thought secure.
Russell, B. (1956). Reflections on my eightieth birthday.
Professor X [...] further admitted that he had no notion how to give a precise definition of logical correctness. Nevertheless, he had always been able to tell which proofs were valid and which were not. What would he gain by learning a precise definition of logical correctness? [...]
[...] he [Professor X] had one further question to ask.
"[...] You are proposing to give a precise definition of logical correctness which is to be the same as my vague intuitive feeling for logical correctness. How do you intend to show that they are the same?" [...]
Actually, not all mathematicians have exactly the same notion of logical correctness. Mathematics is a living, growing subject, and mathematicians do not all work in the same branch of mathematics. Often mathematicians in one branch of mathematics make constant use of some logical principle which is regarded with distrust by mathematicians in other branches. [...]
Although we think that the average mathematician will find that a study of symbolic logic is very helpful in carrying out mathematical reasoning, we do not recommend that he should completely abandon his intuitive methods of reasoning for exclusively formal methods. Rather, he should consider the formal methods as a supplement to his intuitive methods to provide mechanical checks of critical points, and to provide the assistance of symbolic operations in complex situations, and to increase his precision and generality. He should not forget that his intuition is the final authority, so that, in case of an irreconcilable conflict between his intuition and some system of symbolic logic, he should abandon the symbolic logic. He can try other systems of symbolic logic, and perhaps find one more to his liking, but it would be difficult to change his intuition.
Rosser, J. B. (1953). Logic for mathematicians.
[...] the ordinary practice in mathematics illustrates only a partial symbolization and formalization, since part of the statements remain expressed in words, and part of the deductions are performed in terms of the meanings of the words rather than by formal rules. [...]
Propositions of a given mathematical theory may fail to have a clear meaning, and inferences in it may not carry indubitable evidence. [...]
In the case of a formula which represents an ideal statement of classical mathematics, the interpretation cannot constitute a wholly intuitive (or finitary) meaning, but must consist in whatever else it is the classical mathematician thinks in terms of in the informal (or not strictly formalized) development of classical mathematics, i.e. in the development which has taken place historically and takes place currently, when the procedure is not being consciously formalized in the strict sense of proof theory.
Kleene, S. C. (1952). Introduction to metamathematics.
Indeed every mathematician knows that a proof has not really been "understood" if one has done nothing more than verifying step by step the correctness of the deductions of which it is composed, and has not tried to gain a clear insight into the ideas which have led to the construction of this particular chain of deductions in preference to every other one.
Bourbaki, N. (1950). The architecture of mathematics.
[...] what position does proof occupy in mathematics, and how does it influence the so called truth or certainty of our results? [...]
3. Mathematical dogmatism. Now we are probably quite familiar with the fact that mathematical proof is a function of the time. History shows this conclusively - Euclid would probably have complained of the lack of rigor displayed by his predecessors; Weierstrass felt it necessary to reorganize the foundations of analysis; and so on. The present is a time when it seems appropriate to reflect on the new and still uncertain elements that have come into mathematical proof. [...]
But the claim to possess mathematical infallibility, the attempt to set up formalistic or intuitionistic proof rituals - any of these acts and their like, are not, I venture to say, exemplifications of the truly mathematical spirit. [...]
It is natural for the layman to regard our works with awe, to think of us as the possessors of absolute truth, since we have been singularly successful in avoiding contradiction in applied mathematics. But we must not allow this veneration with which we are regarded to tempt us to set up our own mathematical cults or political philosophies. [...]
And I want to point out here what seems to me to be a heartening fact, although I realize that I may be sorely trying some of my listeners, personal philosophies: Namely, that no matter if we do use, frequently, questionable methods of proof, or even make outright errors in proof, we are usually gathering mathematical fruit. [...]
I am quite willing to grant that, with proof or without proof, or with proof by what some of my contemporaries insist is no proof at all, the mathematical theorem is not necessarily a statement of fact or truth in the ordinary sense. But it may be a decidedly elegant and artistic piece of mathematical statement. [...]
5. The role of proof. Now, granted that the mathematical theorem comes from the intuition, what is the role of proof? It seems to me to be only a testing process that we apply to these suggestions of our intuition. We have various kinds of tests, [...] But even though some of these types of proof fail of general acceptance, is there any reason why we should not take successful passing of such tests as evidence that the concept is a possible candidate for admission to the body of mathematical theory? [...]
6. Conclusion. In conclusion, then, I wish to repeat my belief that what we call "proof" in mathematics is nothing but a testing of the products of our intuition. Obviously we don't possess, and probably will never possess, any standard of proof that is independent of time, the thing to be proved, or the person or school of thought using it. And under these conditions, the sensible thing to do seems to be to admit that there is no such thing, generally, as absolute truth in mathematics, whatever the public may think. [...]
[...] I think that a mathematician is to be judged by the quality and reliability of his intuition at least as much as by his ability to prove something. And I am inclined to agree with the statement which I have heard attributed to the late E. H. Moore, that "Sufficient unto the day is the rigor thereof." We certainly owe a lot to those mathematicians of an earlier day whose rigor was rather non-existent from present-day points of view. And if you'll pardon a personal interpolation, if my intuition tells me that a certain theorem is desirable, and seems free of contradiction, I'll prove it in any manner I best can; if my proof makes use of methods or assumptions that certain more dogmatic of my brethren choose to reject outright, I'll prove it just the same [...] At the same time, however, I won't talk about "truth," "absolute rigor," and their ilk - for all I know they are will-o'-the-wisps - ideal conceptions, possibly, but with no natural habitat in the mathematical world.
Wilder, R. L. (1944). The nature of mathematical proof.
Only Dirichlet, not I, not Cauchy, not Gauss, knows what a perfectly rigorous proof is, but we learn it only from him. When Gauss says he has proved something, I think it very likely; when Cauchy says it, it is a fifty-fifty bet; when Dirichlet says it, it is certain; I prefer not to go into these delicate matters.
[alternatively]
He [Dirichlet] alone, not myself, not Cauchy, not Gauss, knows what a completely rigorous proof is, we only know it from him. If Gauss says he has proved something, I think it is likely. If Cauchy says it, one may bet as much in favour as against it. If Dirichlet says it, it is for sure. I for my part prefer not to enter into these delicate issues.
[Er [Dirichlet] allein, nicht ich, nicht Cauchy, nicht Gauß, weiß, was ein vollkommen strenger Beweis ist, sondern wir lernen es erst von ihm. Wenn Gauß sagt, er habe etwas bewiesen, so ist es mir sehr wahrscheinlich, wenn Cauchy es sagt, ist ebensoviel pro als contra zu wetten, wenn Dirichlet es sagt, ist es gewiß; ich lasse mich auf diese Delikatessen[/Delicatessen] lieber gar nicht ein]
Jacobi, C. G. J. (1846). December 21 Letter to Humboldt in: Laugwitz, D. (1999). Bernhard Riemann 1826-1866: Turning points in the conception of mathematics. quoting: Biermann, K.-R. (1988). Die Mathematik und ihre Dozenten an der Berliner Universität, 1810-1933. alternatively in: Pieper, H. (2007). A network of scientific philanthropy: Humboldt’s relations with number theorists. quoting: Pieper, H. (1987). Briefwechsel zwischen Alexander von Humboldt und Carl Gustav Jacob Jacobi.
No comments:
Post a Comment