> a human mathematician would aspire to
Some do. But there's also the notion that a clever trick is a bad explanation.
Some do. But there's also the notion that a clever trick is a bad explanation.
And discovering a bad question leads to the correct question. No?
I think there's a good counterexample to this:
Atiyah/MacDonald proove the Nullstellensatz ultimately by using some trick involving determinants.
They give a very nice theoretical treatment of the content and context of the theorem. But the proof at one crucial point uses techniques that live conceptually outside of this context: While its possible to see that the argument is sound, it does not give a good explanation of _why_ it's true within the context of the theorem.
(You could of course argue that they did not give enough context ... but that's exactly my point: the trick makes the proof work but hides the explanation)
Can't one see it in another way: that the trick illuminates a deeper explanation, connection the theorem's context and the stuff that's conceptually outside of that context. And that the problem is we don't know why the two domains (the context and the conceptually outside of it one) are related and cooperating in this way.
The determinant trick I'm referring to is used in prop 2.4 (in the Version I found via Google).
They use the determinant of the adjugate matrix if I remember correctly... But they just hit the reader with this without any motivation or even naming it.
In fact most mathematicians (myself included!) think the more clever the trick the better the proof! The trick itself being clever is interesting because it often yields a new way of tackling or thinking about your own proofs. A bland explanatory proof that elicits some conceptually “why” is only preferable if it has a reason for doing so - does understanding why yield a new avenue of research? Often then the “why” is quite a clever trick too.
I think it’s a bit the opposite of programming. There you want your solutions to demonstrably not be clever and the code be its own documentation. It’s a different discipline.
I do (of course) understand the issue that non-constructive proofs can be frustrating - and a constructive proof of the same theorem is valuable tool in seeing exactly why a truth is true.
But I guess I've never seen a non-constructive proof (in a space where no constructive proof is available) considered a failure.