No, those are different things. The proposition and its proof. You can assume a proposition and make use of it without a proof.
A proof furnishes the evidence that a given proposition is attainable (e.g., true).
Truly, you could even see this as being composed of three things
- The proposition
- The "stamp of truth"
- (there's a word from Kant that hits this, but I've forgotten it)
- The proof
A proof always furnishes the "stamp of truth", but you could imagine receiving the stamp of truth without receiving the proof. For instance, an authority you trust implicitly tells you it. Alternatively, take a look at all of the zero-knowledge proof work in crypto.
Additionally, there may be many proofs of a single proposition, and thus the "stamp of truth" seeks to represent them as a the equivalence class of proofs instead of giving each different method its own identity. This, formally, is the notion of "proof irrelevance". It flies in the face of computation where we care a great deal about algorithmic concerns, but from a correctness perspective perhaps all you need is the "stamp of truth".
One last way to give color here is to note what the advantage of proof _relevance_ is. In particular, if the structure of the proof itself is visible then we can do things such as _transform_ proofs (think: lisp macro). In this way, we can get more flexible systems which are allowed to port much of a proof's mechanism over to a new target automatically.
Of course, mathematicians demand proof relevance because mathematicians (a) don't trust things they can't see and (b) want to cannibalize proofs for their mechanism and to reuse those mechanisms on other problems. Proof irrelevance is often important for computational reasons: we don't want to carry around the burden of proof (literally) if we don't have to.
A proof furnishes the evidence that a given proposition is attainable (e.g., true).
Truly, you could even see this as being composed of three things
A proof always furnishes the "stamp of truth", but you could imagine receiving the stamp of truth without receiving the proof. For instance, an authority you trust implicitly tells you it. Alternatively, take a look at all of the zero-knowledge proof work in crypto.Additionally, there may be many proofs of a single proposition, and thus the "stamp of truth" seeks to represent them as a the equivalence class of proofs instead of giving each different method its own identity. This, formally, is the notion of "proof irrelevance". It flies in the face of computation where we care a great deal about algorithmic concerns, but from a correctness perspective perhaps all you need is the "stamp of truth".
One last way to give color here is to note what the advantage of proof _relevance_ is. In particular, if the structure of the proof itself is visible then we can do things such as _transform_ proofs (think: lisp macro). In this way, we can get more flexible systems which are allowed to port much of a proof's mechanism over to a new target automatically.
Of course, mathematicians demand proof relevance because mathematicians (a) don't trust things they can't see and (b) want to cannibalize proofs for their mechanism and to reuse those mechanisms on other problems. Proof irrelevance is often important for computational reasons: we don't want to carry around the burden of proof (literally) if we don't have to.