"Finding truth" isn't quite what happened here, though. Finding a contradiction/other invalidation of someone else's proof, doesn't advance the knowledge frontier. It means that there was a flaw in process of proving the original proof, but it doesn't disprove the idea behind the original proof. You'd need your own separate proof to do that—probably a proof by contradiction, of one of the main lemmas of the proof.
The useful skill, here, is one shared by logicians and compilers: the ability to quickly find flaws that invalidate a proof, without needing to fully understand what the proof is trying to prove.
Said skill, if it could be more widely-learned, would be very helpful in iterating toward sound proofs (or impossibility proofs for such.)
But when it's only a skill in the hands of another party external to the one writing the proof, that iterative aspect isn't really there.
Proving that one branch of a tunnel system does not lead to the open air is advancing the knowledge frontier. It's not as 'advancing' as finding a tunnel that does lead to the surface, but it is still useful.
I think I agree with the rest of what you have said.
Sure, but I think the wrong image is conjured by saying "a branch of a tunnel system", since while branches in a real tunnel may themselves branch, they don't tend to branch every few millimeters, the way proofs can branch with every character in possibility space.
Invalidating a proof is essentially what a compiler does when it blows up over a typo in the code you've fed it.
The thing is, most of the time, it is just a typo. The code as-is is wrong, but the code with one character different — the code if "branched" in an alternate direction for just a few millimeters, and then course-corrected back onto the original existing path — is right, and the semantic meaning of the code isn't changed/compromised by that correction.
Finding a logic-level flaw in a (presented) mathematical proof is usually similar: 99% of the time, it's something fixable.
That 1% of the time does still exist; there can be "fatal flaws" in proofs, where the proof's author can't find a way to salvage their proof. But it's not the invalidation of the particular proof, where the knowledge that the proof is unsalvageable (i.e. that there's no path that follows the general "plan" of the branch to get from A to B) gets created. That knowledge is only discovered after much more work by the proof's author, to try to "dig around" the problem, that all turns out to hit other walls.
(Note here that I'm assuming that the proof isn't already believed to be true when it's invalidated. Which it usually isn't; most proofs that get invalidated are invalidated when they're still being circulated as something novel and for-scrutiny, rather than when they're already generally-accepted. If a proof was already thought to be true, then invalidating it would temporarily create "negative" knowledge — it would retract a previous consensus assertion of the truth-value of the proof.)
There are infinite branches that lead nowhere though. This isn’t some data hinting that an effect/correlation doesn’t seem to exist. No useful data or knowledge was discovered here.
A mathematician was exploring a proof, and was shown that the avenue of inquiry they were making could not possible lead where they wanted to go. As a consequence they stopped investigating that path and potentially, as they were shown why that path was invalid, can see possible ways around the problem.
Perhaps the most effective thing a person can spend their time on is pointing people along paths likely to lead to success, and guiding them away from dead ends.
The useful skill, here, is one shared by logicians and compilers: the ability to quickly find flaws that invalidate a proof, without needing to fully understand what the proof is trying to prove.
Said skill, if it could be more widely-learned, would be very helpful in iterating toward sound proofs (or impossibility proofs for such.)
But when it's only a skill in the hands of another party external to the one writing the proof, that iterative aspect isn't really there.