I have posted this in Philosophy SE as well because I feel that it is appropriate both here and there.

As practiced, mathematical proof seems not to be an explicit formal deduction within a formal system. Instead, proof seems to be a sort of critical thinking about things which appear to be necessarily true. The assumptions used in this thinking can be reasonably identified, but they are not explicitly stated at the outset.

Given this, what is the nature of mathematical conclusions in practice? Are they "informal deductions?" Is there any epistemological advantage to explicitly forming mathematical conclusions within a formal system, rather than what is commonly practiced (e.g. you probably haven't proved something like the fundamental theorem of calculus by tracing it back to axioms like ZFC, but maybe it should be done)? If so, why is this not standard procedure in the mathematical community?

I hope these questions are at least relatively clear - and thanks in advance for any insights!


closed as primarily opinion-based by Will Jagy, egreg, zz20s, Shailesh, choco_addicted Apr 16 '16 at 4:34

Many good questions generate some degree of opinion based on expert experience, but answers to this question will tend to be almost entirely based on opinions, rather than facts, references, or specific expertise. If this question can be reworded to fit the rules in the help center, please edit the question.

  • 2
    $\begingroup$ As to tracing back the Fundamental Theorem of Calculus to ZFC, this is can be one in principle by collecting the relevant theorems from the literature, and giving them a unified presentation. Because it is clear that it can be done, and would yield no additional insights, it is not worth bothering with. $\endgroup$ – André Nicolas Apr 15 '16 at 17:51
  • 1
    $\begingroup$ You might find interesting the discussion of realism vs. anti-realism in the Wikipedia article on philosophy of mathematics. I suspect the difference in viewpoints is of little interest to "working" mathematicians because the sufficiency and consistency of such axiomatic systems are "informally" accepted. $\endgroup$ – hardmath Apr 15 '16 at 17:52
  • $\begingroup$ ^Definitely - I've been the philosophy of math wiki page far more than I'd like to admit :) $\endgroup$ – JWP_HTX Apr 15 '16 at 17:58
  • $\begingroup$ @AndréNicolas even if it yields no additional "mathematical" insights, I am not so sure that makes it not worth bothering with. Perhaps there is greater epistemological certainty to be gained by being as explicit as possible from the outset about the assumptions upon which we are basing our reasoning? $\endgroup$ – JWP_HTX Apr 15 '16 at 18:13
  • $\begingroup$ Given a reasonable amount of time, and suitable financial incentives, I could do it. So could tens of thousands, perhaps hundreds of thousands, of others. And there would be the odd error that makes no difference. $\endgroup$ – André Nicolas Apr 15 '16 at 18:21

Basically, it boil down to convenience.

As practiced by mathematicians, a proof is "enough information that should be sufficent to write the formal proof if one would take the time and energy to do so".

When you write a proof, you should be able to explain everything if asked. But often, it's not asked, and the proof concentrate on the difficults points.

Now, if someone ask you to prove a step in your proof, and you're unable to prove it (or give a reference to a valid proof of this step), then your proof is invalid.

So, proofs practiced by mathematicians are not formal proofs, but they are things that could be converted to formal proof if needed

  • $\begingroup$ True, if we restrict attention to explanations given in lectures and papers, but note strong interest in proof automation and verification systems. $\endgroup$ – hardmath Apr 15 '16 at 17:56
  • $\begingroup$ Yeah, so I'm basically wondering if it may be "better" to actually formalize our proofs in math instead of just being comfortable with the fact that they could be formalized. Does it not make sense to strive from the outset for as little ambiguity as possible about the assumptions we use in our reasoning? $\endgroup$ – JWP_HTX Apr 15 '16 at 17:56
  • $\begingroup$ @Searching_for_a_foundation : the problem is that it become very heavy very fast. The idea is that you trade useless precision for efficiency. The keyword is useless. If you think there's an ambiguity, don't hesitate : formalise more ! $\endgroup$ – Tryss Apr 15 '16 at 18:12
  • $\begingroup$ @Tryss - yes, it does become very heavy very fast! But I think "how heavy" is an interesting question. Is it truly impossible for a human to do this? Maybe a computer could do it? In any case, I do see your point - it would be so vastly complicated to trace all of math up from axioms that for all intents and purposes, if there doesn't seem to be any real ambiguity in your work, then you should feel comfortable about it. $\endgroup$ – JWP_HTX Apr 15 '16 at 18:17
  • $\begingroup$ @Searching_for_a_foundation : yes, that's a task perfectly suited for a computer. There are some projects that aim to give formal proof of the usual theorems in analysis $\endgroup$ – Tryss Apr 15 '16 at 18:22

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