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!