How should one properly characterize mathematical conclusions?

Question

I am a mathematics graduate student, not a philosophy student, so please bear with me. However, I am interested in investigating what exactly it is that I spend the majority of my week doing!

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!

Answer 1

It seems to me that a proof is - or at least tends to be - something that mathematicians in the relevant field feel could be formalised. Formalisation would involve explicitly stating those steps that are otherwise implicitly accepted as valid. The problem is that doing so would probably obscure the core result in a welter of detail, such that reading proofs would effectively waste readers' time by making them wade through results they've already long-accepted. This is probably why formalisation is not "standard procedure in the mathematical community".

Having said that, formalisation is gaining more attention due to the increasing interest in computer-assisted proofs; cf. this post by Mike Shulman on computer formalisation. In particular, note Shulman's comment about "an additional benefit to doing mathematics with a proof assistant (as opposed to formalizing mathematics that you’ve already done on paper), which I think is particularly pronounced for type theory and homotopy type theory."

Answer 2

Your proof may not be fully formal, but the expectation is that it should at least be falsifiable. If it were fully formal, then it would not just be falsifiable, but also verifiable. If somebody goes through your proof and points out mistakes or holes, it is expected that you acknowledge mistakes, and either acknowledge holes, or explain how the holes can be filled.

There are more expectation both on you as the author of the proof, and on your audience for the proof. If your audience just fails to notice your proof, or has better things to do then read and check your proof, then your proof is not a real mathematical proof yet. But if there are readers, and they point out mistakes or holes, then the author should try to respond appropriately. The readers will notice if you don't respond properly to questions and objections. It will sort of feel to them like playing chess against a kid that doesn't yet fully understand the rules of the game. They might try to explain the rules, but often the outcome is that your proof is simply ignored, and no longer considered to be a piece of mathematics.