4 ms·
I wonder if e.g. using constructive math would make things easier since every step of a constructive proof is understandable.
by adamnemecek 6y ago
I wonder if e.g. using constructive math would make things easier since every step of a constructive proof is understandable.
- Koshkin 6y agoMy understanding is that since any mathematical proof can (in principle) be reduced to manipulation with formal objects (symbols), it’s always “constructive.”
- hintymad 6y agoNot really. Check out the proof of Hilbert's Nullstellensatz. He got tons of criticism for proving the existence of a relation without constructing that relation.
- Koshkin 6y agoBut he did construct the proof! (So, the argument can only be about what axioms the proof is based on.)
- alexanderchr 6y agoThis is not what constructivity means in mathematics.
- Koshkin 6y agoWhat I was objecting to was that constructive proofs are somehow easier to understand.
- pointedset 6y agoUnfortunately, constructive vs classical (vs linear, etc.) applies to proofs, but this is really about definitions. Proofs can be correct or incorrect pretty straightforwardly, but definitions being correct or not is really a matter of taste. (And as someone who's been formalising some mathematics in Lean recently, definitions are so much trickier to get right than proofs!)