Comment by mb7733
2 days ago
Those are all good questions, but I don't really understand what alternative you or the OP are looking for actually resolving an untrue conjecture, besides a counter example.
2 days ago
Those are all good questions, but I don't really understand what alternative you or the OP are looking for actually resolving an untrue conjecture, besides a counter example.
I would frame it differently. The existence of compact counterexamples to a true-seeming conjecture suggests that there’s some deeper understanding waiting to be discovered. Fuzz testing for theorems, if that makes sense. I hope mathematicians in 2036 will be able to explain in detail why the Jacobian conjecture was false and identify which similar, true conjectures the community’s intuition was pointing towards.
We can take a simpler example. Let's say someone conjectures that all linear maps are isomorphic if they have the same domain and codomain*. A counterexample is easy to find, but true insight would be to notice that all linear maps with the same domain and codomain that are not isomorphic map some non-zero elements to zero. That is much more interesting than just finding a counterexample. Although, that isn't to say that finding a counterexample is not very interesting.
*statements only apply to maps whose domain is finite-dimensional
I suspect an AI, possibly a successor to current LLMs, will achieve that by the early 2030s. It might help illuminate many mysteries in math and beyond for us all.
There are many cases where it's possible to prove that counterexamples must exist, without identifying a specific example. This kind of proof provides more insight into the problem than simply finding a counterexample.
Constructivists would surely disagree!
As a constructivist: we don't disagree :) We just distinguish between "don't disagree" and "agree." Constructive mathematics says it's fine if you want to claim that there's not no counterexample -- you just can't use that in a situation that demands an actual counterexample (like an algorithm that produces a result). This tends to guide people towards looking for results that don't require this kind of indirection, since they apply more broadly and in more kinds of logics -- orthodox constructive results are kind of a lowest common denominator of consistent truth and remain broadly compatible with most axioms, while nonconstructive results often fail in particular models. Which seems like a pretty sane stance to me, but maybe I'm too thoroughly indoctrinated to see how unreasonable it is :P
(Note that this is about excluded middle. There ARE constructive logics with interpretations of excluded middle, e.g. some forms of classical linear logic, but they do not play as nicely with other logics. Constructivists often reject even weak forms of choice for largely the same reasons--there are some forms of choice that are constructively valid in some logics, but these results often fail to hold true in more conventional logics. And the same is true for a whole host of related notions that proof assistants like Rocq reject by default, propositional extensionality (which says that two proofs of the same proposition are equal) and function extensionality (which says functions are equal whenever their results are equal on all the arguments in their domain -- which might seem obviously acceptable until you realize that it's false in most programming languages!) being prominent but much less discussed examples. It's all about remaining broadly compatible with lots of different types of reasoning, not because people think the reasoning is invalid per se).
2 replies →
In a constructive system, it’s often possible to refute a universal proposition without exhibiting a counterexample, by proving that the proposition implies falsehood.
The constructivist will still object that you can’t, from that, conclude that “…therefore a counterexample must exist,” without actually providing a counterexample. But the general principle I was describing still applies - a proof often gives you insight that an example by itself doesn’t.
6 replies →