[ak_111]

Unlike the unit distance problem, the impressive thing here is that it is a proof rather than a counter-example.

However, it seems the proof is extremely concise so it seems that it is exploiting a clever trick that somehow all the experts missed.

So not to dunk on this amazing result (or move the goal post), but it seems now the only achievement that AI hasn't managed in mathematics is presenting an autonomous "theory-building" proof of an open conjecture. That is a proof that requires creating a substantial new theory (developed say in at least 30+ pages) to crack an open problem.

[jvanderbot]

It is very concise, and reads precisely as you suggest: to exploit properties already discovered and therefore combined in a novel way.

I'm just delighted by the prose. It reads like an old paper. The ones that were just straightforward theorems with proofs that do exactly what they say.

[lubujackson]

In my (very) limited use of GPT-5.6, I have noticed it is quite concise in general, and significantly better at abstract thinking. Doing a PR review of a large change it was interesting to see Fable and 5.6 mention a few similar points with Fable much more long-winded and less readable, while 5.6 caught more "second-level" concerns and Fable more "in the code" concerns, so they both are quite useful in concert.

In general, I would not be surprised if 5.6 was a much better tool for high mathematics than Fable based on the abstract thinking. For my dev workflow, I have flipped my approach from planning with Opus 4.8 high and implementation with GPT 5.5 to planning with 5.6 high and implementation with Fable medium (and I might even drop to Fable low). This is only on the company dime, of course.

[satvikpendem]

This has since been the case with recent models from OpenAI vs Anthropic, seems it's a matter of their philosophies embedded into the model, much like Conway's Law.

[dannyw]

Probably comes as a side effect of optimising and post-training for token efficiency.

Fortunately, OpenAI APIs expose the verbosity parameter, which is separate to effort. If you want longer responses, you can. Or just prompt it.

[greenavocado]

I use GPT 5.6 as default and subtask agent and Fable as Advisor with Oh My Pi harness

[qarl2]

> However, it seems the proof is extremely concise so it seems that it is exploiting a clever trick that somehow all the experts missed.

Why is that a "however"? My reading is that it found a genuinely new solution that is both elegant and previously missed.

Seems like exactly the kind of result a human mathematician would aspire to.

[Garlef]

> a human mathematician would aspire to

Some do. But there's also the notion that a clever trick is a bad explanation.

[qarl2]

Hmmm... seems to me that if you can find a solution without creating the desired explanation - then that's a problem with the original question - not the solution itself.

And discovering a bad question leads to the correct question. No?

[Garlef]

> then that's a problem with the original question - not the solution itself

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)

[wbl]

I was baffled enough by this comment to take my copy and look. The Nullstellensatz is an exercise late in the book long after Noetherian rings are introduced and they don't even do the Rabinowitz trick in the hints as they have enough theory to hit it the hard way. Determinants are nowhere to be found.

[Garlef]

It's been a few years (~ 15) since I read it.

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.

[coldtea]

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

[qarl2]

Ah... is this just the difference between a constructive and non-constructive proof? Is that the distinction you're making?

[fnordpiglet]

But a proof isn’t an explanation it’s a proof. Proof by assuming the opposite is true and demonstrating a contradiction is very indirect and not at all directly explanatory yet it’s a proof non the less. The goal of proofs is to demonstrate something to be provably true, not expository knowledge gathering.

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.

[qarl2]

Thank you for the validation. I only dabble in mathematics - so it's reassuring to hear what I remember - a clever proof is still considered a positive thing.

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.

[calf]

Is this what the prompt means by proof strength gap, or is that something else entirely? (Sorry not a mathematician.)

[ak_111]

clever tricks has value for sure. But the main way progress is done in mathematics is by building new theory, the proof of Fermat's Last Theorem is much more important because of the math it created to solve the problem, rather than actually solving the problem.

[qarl2]

Right. I think I understand - this question was expected to produce a new theory and the clever solution avoided that.

Like I said below, I think this is a fantastic result. It discovered that this question really wasn't asking the right question. That's a determination that has eluded the humans examining the problem - and a real step forward - albeit not the hoped-for step.

No?

[pfdietz]

That depends on the branch of math. Combinatorics is trick-oriented. Maybe this is why AI has done well in that.

[vessenes]

Grant Sanderson recently distinguished mathematicians that create syntax (he might use the word ontologies in some circles) from those who manipulate it on the Dwarkesh podcast. I liked this delineation a lot. We seem to be at ‘manipulating syntax’.

Creating useful ontologies still seems a ways off here. Not to complain about this awesome result, just to think about where some future goalposts might be laid (and of course complained about / discussed at length when reached)

[moomin]

For comedy’s sake, I asked ChatGPT 5.5 about the significance of the problem and the chance that 5.6 would solve it with a three page solution. It said close to zero.

I invited it to search the internet and it remains extremely sceptical.

[perching_aix]

Have you tried... giving it the proof?

I tried to use Sol to:

- double check the proof (provided it with the prompt and proof artifacts)

- double check some of the claims made in this comment section (no math involved newer than 30 yo, no human contribution or review, no mathematician affirmations, proof assistants not being developed enough in this area to support machine checking a proof like this)

- check for any mathematician feedbacks

It stalled out (bad first impression much? lol). I then retried with 5.5, expressing the same request and my personal skepticism, and it returned to me with cautious optimism and no obvious issues found.

I think the fact that I provided it with the actual artifacts in question vs. you simply asking it to speculate about them is a really interesting UX difference. Like certainly, a coveted 50 year old math problem having a few pager proof is not going to be very likely. But then skim reading the proof by a frontier model is not going to yield any obvious issues either. Both responses are perfectly defensible given the context (I don't necessarily think these qualify as sycophancy), but we'd walk away with entirely different impressions if we didn't know about each other's requests.

And I'm not even trying to suggest you were wrong to not approach it in the ways I did. It's a perfectly reasonable and human way to prompt it the way you describe. It's just not the way I'd do it, but I have a hard time articulating why. And it's clear that the model was never going to help with this difference either.

Half a century of computing, and we're still trying to make the machine think on the users' behalf :)

[WhitneyLand]

The prompt does matter. They specifically told it to assume a proof exists so it would not too easily dismiss the possibility.

[moomin]

I considered it, but I figured that whatever I did there would be inconclusive. Instead I tried to figure out the blast radius of this being proven, and I didn’t get very far with that either.

[brokensegue]

Fable told me

> Verdict: I checked every step and found no error. The argument appears to be a correct proof of the Cycle Double Cover conjecture, modulo two standard cited results (the reduction to loopless cubic graphs and the Jaeger–Kilpatrick 8-flow theorem, both real and well-established).

> Two caveats: this would settle a ~50-year-old open problem in three pages, so it deserves independent expert scrutiny regardless of my check; and I couldn't reach the web from here to confirm the paper's provenance or any community response, so I can't tell you its status beyond the mathematics itself.

[DroneBetter]

the unit distance problem's paper was human-summarised and condensed significantly from the initial LLM output, so it seems the model did do some theory-building there (possibly providing motivation for the clever trick as a natural deduction, at least in its eyes) before humans cut off all the chaff; I imagine the development was similar here.

[dooglius]

I wonder if in each case they had parallel sessions, one trying to prove, one trying to find a counterexample

[throw310822]

> seems that it is exploiting a clever trick that somehow all the experts missed.

Exactly, "clever". Isn't that the whole point?

[koolala]

A clever trick is way better than a stupid trick yeah. I don't get complaining about a concise elegant solution either unless a specific problem with the actual proof was brought up.