If someone disproved the Riemann hypothesis, it would be the biggest math story of the century -- certainly since the proof of Fermat's last theorem, I am sure.
I also think that working out the consequences of a conjecture being true is _indistinguishable_ from attempting to disprove the conjecture. How could you possibly work out something like a proof (or disproof) by contradiction without doing that? Really working toward a proof in general is the same as working toward a disproof in almost every case I can think of. An exhaustiveness proof is also a search for a counterexample, etc.
Sometimes a statement A is a non-trivial consequence of both a conjecture B and it's negation independently. So in a technical sense A doesn't take you any closer to a proof or disproof of the conjecture in question (and it can be difficult to tell whether your consequence is of this type or not).
Believe it or not, constructive math actually does have a LEM, but a derived one. Any computable value can be shown to either equal or not equal another. Only for uncomputable predicates does the absence of LEM result in our inability to conclude x from not not x.
If I try to do it directly I keep using the law of excluded middle accidentally by assuming "A or not A" (or some consequence like contraposition if I try and apply your linked theorems).
Theorem foo: forall P Q: Prop, (P -> Q) /\ (~P -> Q) -> ~~Q.
Proof.
intros.
destruct H.
assert (~Q -> ~P).
intros. intros contra. apply H in contra.
contradiction.
intros contra. apply contra. apply H1 in contra.
apply H0 in contra. assumption.
Qed.
First of all, contraposition (in the "adding a not" form, not in the "removing a not" form) is an intuitionistic theorem. And it is getting used here.
So we are saying, use contraposition (here, prove contraposition) on P -> Q, to get ~Q -> ~P.
Now, to show ~~Q, we want to show that ~Q would lead to a contradiction. (In Coq, ~X is literally defined as X -> False.)
So, suppose ~Q. Then from that contraposition conclusion, we have ~P. But by hypothesis, ~P -> Q, so then Q. Then we have Q and ~Q, which is a contradiction. (To explicitly use the contradiction to deduce False, we can say "we have Q -> False and we have Q, therefore we can deduce False".)
OK, I guess that wasn't so hard! Anyway, getting the contraposition consequence is actually very close to getting the desired result here. You just have to think in terms of "~~Q" meaning "~Q implies a contradiction". :-)
For example, some forms of De Morgan's Law work but some don't!
These are valid intuitionistically:
(P /\ Q) -> ~(~P \/ ~Q)
(~P /\ ~Q) -> ~(P \/ Q)
(P \/ Q) -> ~(~P /\ ~Q)
~(P \/ Q) -> (~P /\ ~Q)
(~P \/ ~Q) -> ~(P /\ Q)
~(~P /\ ~Q) -> (P \/ Q)
~(P /\ Q) -> (~P \/ ~Q)
~(~P \/ ~Q) -> (P /\ Q)
(forall x, P x) -> (~exists x, ~P x)
(exists x, P x) -> (~forall x, ~P x)
~(exists x, P x) -> (forall x, ~P x)
~(forall x, P x) -> (exists x, ~P x)
I also assumed many mathematicians utilized the strategy of attempting to disprove something as a way to reveal the proof. Sort of like how the best chess players tend to spend most of their thinking time mentally challenging their planned move as opposed to novice chess players who tend to look for reasons confirming why their move will be a good one. Is this not the case?
The author seems to have completely missed the actual reason we find conjectures interesting: we're asking ourselves, "do we have the techniques to prove this kind of problem?" That's the fundamental reason disproving a conjecture is less celebrated than proving it, because disproving is often done by finding a single counterexample, which doesn't teach us much about our proof techniques -- unless, of course, the process of finding that counterexample was particularly new and interesting!
The most interesting question to ponder with a conjecture is not "is this true?", but rather "why is this hard to prove?". The most boring answer to the latter is "oh, because it's false", while the most exciting answer is "because we were missing this fundamental idea that can spawn an entire new branch of mathematics." It's all about the journey, not the destination.
The fact that the human mind is capable of searching for new mathematical theorems specifically here instead of there, is quite interesting. It's as if a skilled mathematician has knowledge that is bigger than math itself.
Penrose used this as argument for the special nature of consciousness, wrongly - it probably makes more sense to remember how the way the human mind is not exact and produces errors all the time plays a huge role in a creative process. And luckily we can amend the human mind by social processes that help eliminating errors again.
This way, a conjecture can be thought of as a claim to truth in a competitive environment and that would explain why proving the truth is regarded so much higher.