proofs by counterexample are effective but ultimately unsatisfying. they get you to an answer but they don't help help you understand and bend you r mind into seeing how the math works and lead you on to the new set of questions.

and for now as long humans are going to judge of what counts as an elegant or illuminating proof, there's going to be work for human mathematicians

▲

remus 18 hours ago | parent | next [-]

I would only agree partially. There are counterexamples that are not illustrative, but it is fairly common that in thinking about how to construct a counterexample you gain a more thorough understanding of the original problem and at least one fundamental issue which prevents the conjecture from being true.

	▲	fuglede_ 8 hours ago \| parent [-]
		Right; see Lakatos. In its roughest form, you study the structure of whatever counterexamples you find, add those as (negated) preconditions to your proposition, rinse and repeat until you have a true statement. If the proposition remains useful, you now have a new definition.

▲

throwaway676712 14 hours ago | parent | prev | next [-]

Counterexamples are literally the only way to show a "for all" statement is false. (Non-constructive proofs by contradiction work by showing a counterexample must exist.)

Also, 'brute-force' style attacks where one simply feeds the input into the computer and it yields a solution are nothing new and certainly predate LLMs: https://en.wikipedia.org/wiki/Euler%27s_sum_of_powers_conjec...

Hell, one could even go further into the past and refer to the thankless work of pre-computer era mathematicians who sweated over manual calculations in order to disprove various prime related conjectures: https://en.wikipedia.org/wiki/Mersenne_conjectures

You seem to have an objection to non-intutionist mathematics in general, a position that was once held by many an illustrious mathematician but is relatively fringe in the contemporary academic community. Mathematical facts don't have to be intellectually satisfying or make sense to you, the human, rather it is up to you to wrap your mind around discovered mathematical facts.

▲

mb7733 18 hours ago | parent | prev | next [-]

Are you thinking of proof by contradiction, which is rejected by constructionism?

[Dis]proof by counterexample is the most straightforward way to show a statement to be false. What better way is there to disprove a general statement like 'all x are y' than finding an 'x' that isn't 'y'?

▲

SpicyLemonZest 18 hours ago | parent [-]

It’s very straightforward, but it often doesn’t (and here didn’t) fully satisfy the curiosity that was embedded in the original problem. Why did the Jacobian conjecture seem to be true? Is there some underlying symmetry that’s very slightly broken? Or perhaps there’s all kinds of counterexamples, and the intuitive pattern is only real for certain kinds of functions which happen to predominate in our intuition. Then how should we adjust our intuitions to better capture the space of possible polynomial functions?

▲

mb7733 18 hours ago | parent | next [-]

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.

▲

SpicyLemonZest 17 hours ago | parent | next [-]

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.

	▲	ChadNauseam 14 hours ago \| parent \| next [-]
		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
	▲	nopinsight 15 hours ago \| parent \| prev [-]
		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.

▲

15 hours ago | parent | prev | next [-]

[deleted]

▲

antonvs 6 hours ago | parent | prev [-]

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.

▲

mb7733 3 hours ago | parent [-]

Constructivists would surely disagree!

▲

Jweb_Guru 2 hours ago | parent | next [-]

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).

	▲	mb7733 an hour ago \| parent [-]
		Maybe I was unclear. The part that I meant a constructivist would disagree was the subjective part: "This kind of proof (existence of a counterexample) provides more insight into the problem than simply finding a counterexample." I find it hard to believe that a constructivist would agree that across the board, proof of existence of X is more interesting than a construction of X. Isn't that the point!?

▲

antonvs an hour ago | parent | prev [-]

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.

	▲	mb7733 an hour ago \| parent \| next [-]
		To roughly repeat myself from a sibling comment: I may have been unclear. I didn't claim that the only way to disprove something in a constructive system is to produce a counterexample. The part that I was referring to was the last statement from the OP: that "a proof of existence of a counterexample necessarily provides more insight than a counterexample". I can't imagine a constructivist would agree with that in general.
	▲	Jweb_Guru an hour ago \| parent \| prev [-]
		I think the constructive position is basically that people's entire issue with lack of excluded middle being absent is just that people like being able to say "P" instead of "~~P" because it sounds better, considering you can prove ~~P for all the classical propositions that use excluded middle.

▲

inigyou 4 hours ago | parent | prev | next [-]

You, right now, have the ability to spend a few weeks studying the Jacobian conjecture and its counterexample and write up a blog post about what you think is special about this counterexample.

▲

murphyslaw 10 hours ago | parent | prev [-]

Isn't the fact that you now know that the conjecture is false a huge help? At least it will help convince people to look at the conjecture more closely, no?

▲

delecti 17 hours ago | parent | prev | next [-]

You could spend the rest of your life coming up with conjectures that look elegant but are ultimately false. Disproof by counterexample only works if it's false, and we shouldn't be satisfied with a false conjecture to begin with.

▲

SonOfLilit 6 hours ago | parent | prev | next [-]

The counterexample in the news cycle today helps better understand how the math works. I can't think of one that doesn't.

▲

linzhangrun 14 hours ago | parent | prev | next [-]

> and for now as long humans are going to judge of what counts as an elegant or illuminating proof, there's going to be work for human mathematicians

Considering ChatGPT was released only three and half years ago, and LLMs could do high school math only less than two years ago, I think this "for now" will not last very long.

	▲	bluGill 3 hours ago \| parent [-]
		> Considering ChatGPT was released only three and half years ago ... Or are they approaching an asymptotic limit?

▲

veunes 9 hours ago | parent | prev | next [-]

Elegance may not remain exclusively human forever but usefulness probably requires more than correctness

▲

moralestapia 17 hours ago | parent | prev | next [-]

Not much worth in understanding a statement that is wrong and has been shown wrong.

Unless you want to spend time "proving" that 2 * 2 = 1.

▲

reinitctxoffset 9 hours ago | parent | prev | next [-]

Seems like a breakdown on the incentives / imperatives in the field? I hope that's not an over bold guess from a non-mathematician.

Couldn't people in principle continue to study a problem that's only been shown to break at one point? Prove something adjacent, or slightly weaker, or elaborate the counter example into a powerful explanatory framework?

▲

taneq 18 hours ago | parent | prev [-]

Maybe I’m just not pure enough but I find the whole concept of proof by counterexample to be elegant, and I don’t see why proving that something must be true is superior to proving that it can’t be false.

▲

chowells 18 hours ago | parent | next [-]

It's elegant if all you're concerned with is whether a conjecture is true or false. Answered, move along!

But mathematics is not a collection of facts. Mathematics is the study of abstraction. And what do you learn from a single data point? What can you abstract from that?

That's why just being a counterexample isn't really interesting. There has to be more than "counterexample" for there to be something to abstract. Was it generated from an analysis of the problem? Can the counterexample be generalized to explore the problem further? Is the counterexample a surprise in a way that suggests something is missing from current understanding?

Being a counterexample doesn't mean that something isn't interesting to a mathematician. But it's also not the interesting part.

▲

ATMLOTTOBEER 15 hours ago | parent [-]

You’re smuggling in a frame here which isn’t obviously true: that mathematics is not just a collection of facts

▲

chowells 11 hours ago | parent [-]

You have a weird definition of "smuggling". I say it outright. Because I follow it up with a description of the actual practice of math: it's the study of abstraction. That's not a frame. That's just what math is.

	▲	im3w1l 4 hours ago \| parent [-]
		I think the nature of mathematics is an interesting question without one clean answer. To present a radically different view of mathematics: It's a game of string transformations, where the goal is to produce specific strings given a set of rules. The (syntactically valid) strings would correspond to statements, a producible string a theorem, and the production the proof.

▲

bananaflag 18 hours ago | parent | prev [-]

You mean proof by contradiction, which is something different.