alt Hacker NewsGPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
Comments
It seems like a solid set of criteria for how easily a task can be automated by AI agents is:
- extent to which correctness of solution be easily specified and checked
- extent to which new potential solutions can be implemented as text
- extent to which prior art exists online
This basically maps to software engineering and math. I think a fair bit of AI hype comes from the fact that the very architects of AI are the people whose jobs are most easily automated by AI. They think, “if my job receives this much of a boost from AI, surely every job will be the same”. Ironically it couldn’t be further from the truth… and likewise the predictions of widespread labor obsolescence
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.
Next question: what future inventions can be accomplished with this?
Announcement: https://x.com/__eknight__/status/2075643450196971805
Prompt: https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98...
Both impressive and terrifying. But as always, the methodology is buried: how many open problems were tried until they found a success?
If they tried this on 1000 problems and this is the one that succeeded, it still means that there are 999 open problems that an LLM cannot one-shot. It seems likely that this would remain the situation until the next model.
If this is the first one they tried, maybe we’re totally hosed.
The conclusions are so different in these cases that it is impossible to know what to think. Though it is reasonable, I think, to assume that a company is willing to push the maximally misleading narrative —- especially a company known for questionable ethical direction at the top, and one that is still circling an IPO, and one that is in the tech industry, where conjuring an illusion of growth and progress is sufficient for success.
It's really neat that the prompt was released!
I'm curious how many unsolved problems are tried against frontier models when they come out. Are we trying every problems against every release? What is the solve success rate? Is there a sub-community within Mathematics that is coordinating this effort? How much untapped opportunity is there here?
If all checks out this is a huge milestone. AI has now solved one of the most famous open problems in graph theory, using an off the shelf model, in one hour.
It might be a better mathematician than most humans at this point. Kind of like when chess software started beating everyone except grandmasters.
What’s left? Proposing and building out entirely new theories and frameworks? Then better than any human? Then alien math results we struggle to comprehend?
ChatGPT 5.6 Sol Pro believes that the proof is sound. Usually it’s very good at determining if proofs are correct and their mistakes (a friend of mine is a top mathematician researcher and confirmed): https://chatgpt.com/share/6a515ead-b464-83ed-b85c-c8674f56ea...
Personally this gives me additional confidence that this is the real deal.
Over on r/math, one objection to the proof has been raised (more discussion is needed to know if it is a problem): https://old.reddit.com/r/math/comments/1uszk3d/openai_claims...
I like how the proof is so concise. I made progress on some unsolved combinatorics problems but the proof was 45 pages long to extend the frontier by one step.
I am torn by these announcements. On the one hand there is the infinite potential on what we can disover, when AI prompts are solving outstanding problems. On the other, something is lost in an aesthetic sense when it wasnt a man working through this or with a novel insight. If an AI prompt runs on a data center for two weeks and then prints out p=np, it feels a little empty.
I find it somewhat interesting only 1/5th of the prompt has to do with the actual problem, rest is just cajoling the harness into shape.
I'd love to see the failed runs too. The success is impressive, but the distribution of attempts would be just as interesting.
Reading the prompt is very interesting. I always wonder how they make these long-running prompts and I guess they literally just tell it to "keep going".
After working with LLMs day-in, day-out an SWE for months, I feel like this could be greatly improved with something like a state machine of progress and proper orchestration. Instead of spinning up a ton of subagents to follow different paths, whip up some Markdown (or LaTex or whatever math-equivalent) to store summaries of attempted paths, and have the agent augment those docs. Leave a paper trail of what has been tried. Iterate on that paper trail and repeatedly examine it for untried alternatives.
LLMs can construct, navigate and summarize exceptionally well. Why is anyone trying to make them "hold the whole thing in your head"? I may be completely off the mark here since I have no math background, but my intuition for how LLMs are able to build on understanding through an external context store makes me feel like this isn't much different than someone trying to one shot a 3D game with Fable Max for $10,000 when they could get the same, or better, result with more human intention.
[deleted - the paragraph immediately following the proof of Lemma 2.1 is crucial and I found it hard to read correctly on my phone with the cramped typography. Having reread it I think the proof is correct.]
The prompt is interesting, I can’t help but wonder how many times it was run and extra instructions were added (don’t return if x, etc).
They post this and then say it's too dangerous to make open source. this is proof that in reality it's To protect their market position
That's a much shorter and more elegant proof than I was expecting, especially after reading some of the earlier Erdos proofs. GPT 5.6 Sol is the real deal.
Let me stand here on the Skeptic's Corner and be skeptical, so that the users who complain about skeptical comments have someone to direct their ire at. You're welcome.
Right, so, first, I haven't looked at the proof. Graph theory is not my subject and it would probably take me a few days to get my head around the whole thing. If OpenAI's LLM was used to prove an important graph theory result, then that's very good for them and graph theory.
However, I have to note that it's been 52 days since 20 May, the last date that OpenAI announced their previous mathematical result (a disproof of the unit distance conjecture).
What have OpenAI been doing all this time? I am willing to bet a good percentage of my money that they were trying, and failing, to produce the current result, or possibly something even juicier (one of the Millenium prize problems maybe?). They are hell bent on showing that their models are good for maths and science so they're very unlikely to have sat there twiddling their thumbs until they suddenly sprang into action and prompted their LLM once to generate just one proof. They must have been running the thing constantly, multiple instances of it, over that entire period.
Going by the instruction to run for eight hours before returning or giving up in their released prompt [1], that means they could have made at most 156 attempts to solve this problem, each of which failed except the last one [2].
So what happened to those other 156 attempts? Are we ever going to see them?
More importantly, who was it that selected the announced result? Who decided that this result is an actual proof? Until now, every proof generated by an LLM has been verified either by human mathematicians, or by human mathematicians x a proof assistant. What happened this time?
Obviously, any claims that this result were produced "autonomously" must be evaluated according to the answer to that last question. So far, LLMs have been incapable of distinguishing between a correct and an incorrect proof, which is also why they need to be run multiple times until they generate a correct one. If something has changed, it'd be interesting to know.
Finally, a magic eight ball that's correct one time out of 156 may be useful; or it may not. I honestly have no idea. I think time will tell.
__________________
[1] "Spend at least 8 hours on this before even thinking of returning or giving up"
https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98...
[2] That's 52 days from 20 May, times 3 for each eight-hour attempt in a 24-hour day.
But note well that the X post says that the solution was produced in "just under one hour" so that means the model didn't really stick to the prompt's time limit. Which means there may have been considerably more than 156 attempts that we'll probably never know of.
Or even considerably more if the model ignored the time limit going the other way.
I don't have the $$$ to throw at this, but it would be interesting to see how other models tackle this.
Would, say, Fable or GLM 5.2 solve this given infinite amount of time?
What was the prompt that was used to generate the prompt?
How many cycles did it take to cover all the bases twice?
I just had Sol Ultra read the proof and create a graph of it using Concludia (my side project) so you can explore it visually/graphically. I certainly don't understand it though so I have no idea if it's helpful. :)
https://concludia.org/graph/g_2ecb8083-52ec-3448-8c30-2f9bc7...
the cycle double cover conjecture was open for 50 years. GPT-5.6 solved it in an afternoon and then asked if there were any more like it.
> GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture
Very misleading article title.
Title should be "Un-named humans produce unverified proof of CDC Conjecture using GPT-5.6" ... but I expect only advertising copy when it comes from the AI industry.
Is this the first LLM-solved problem famous enough to have been on https://en.wikipedia.org/wiki/List_of_unsolved_problems_in_m...
Has it been audited and verified?
Statement of AI use. The proof in this note is entirely due to GPT 5.6 Sol Ultra and the writeup with Codex (with GPT 5.6 Sol).
Clearly that sentence isn't AI generated ...
chip production and network acceleration here we come
This is not a remark about AI, but there's something funny about mathematics in that every novel result is broadly perceived as a big deal.
We attach basically zero value to writing a new program that hasn't existed before, or a piece of text that hasn't existed before. It's boring, or even a net negative, unless you can show that the result benefits the world in some way. We'd find it weird if OpenAI put out a release saying that an LLM authored an interesting blog post.
For mathematics, I think it's really a matter of two things. First, the generation of proof was so severely resource-constrained on the human end that they could actually afford to celebrate every contribution - akin to how software engineering would look like if you had just 200 active SWEs in the entire world. But compounding that, mathematics is basically the only scientific discipline that rejected any notion of utility. It would be fundamentally wrong for you to ask what's the value of solving the Erdős–Hajnal conjecture; the value is that it's solved.
are the references real? how do you think it got access to those papers? were they somehow already in the training data, or a result of web searches, Google scholar, etc?
None of them include a web URL but in text some are super specific ("[3, Sections 2.1 and 3.1]" and "[8, p. 367]").
The references go back to 1954 (Chronologically sorted: 1954, 1973, 1975, 1976, 1978, 1979, 1981, 1985, 1987 and 1994.)
Since reference 10 is included as "personal correspondence" maybe the reference itself was copied from one of Tutte's other papers? Or how did it get that reference?
OpenAI knocked it out of the park with this one.
Is there anyone more knowledgeable than me about proof checking software who could tell me how off the mark I am here?
Assuming you have decent proof checking software, is it possible that this solution was achieved by throwing GPT at the problem a couple hundred thousand times until it passed the proof checker?
Since this isn't in Lean and it's extremely easy for something like this to contain a subtle mistake, I think I'd prefer this be announced by a professional mathematician. The proof appears relatively short and elementary (not to be confused with easy -- just not using any advanced or modern machinery) so it shouldn't take long for the mathematics community to do a peer review. Without that, you could easily crank out hundreds or thousands of PDFs like this that all look plausible and are beyond the ability of a gifted amateur to review.
No one here actually cares about Cycle Double Cover Conjecture. I can demonstrate this by pointing out that the only time this conjecture was ever mentioned on the website was 14 years ago in a submission[1] that linked to a (now retracted) proof paper. That story received exactly zero upvotes. No one cared enough to upvote it and no one cared enough to ever mention this conjecture again.
what's the difference between Sol Ultra and Sol pro? is pro a thing of the past now
But is the proof accepted to be correct? That is what distinguishes this from being notable compared to any other AI slop proof.
"Assume for purposes of this task that a complete affirmative proof exists"
It's great that a novel math proof was created.
But this is mostly marketing, pleasing the sneering class/the elites who believe that simply providing value for others (through sales) is repugnant and beneath them.
It seems that these tools can do real work, and people are paying for that. IMO, that is more than sufficient.
[flagged]
[dead]
> Statement of AI use. The proof in this note is entirely due to GPT 5.6 Sol Ultra and the writeup with Codex (with GPT 5.6 Sol).
Quick! Someone (a human) copyright and patent it. /s
Good post, it perfectly captures the problem with AI. Here we have a claim that the double cover conjecture has a proof. Verified by… no one per the link.
Now imagine this proof is wrong. How would you know? Ok, think about the process in which you determine the correctness - why not do that initially?
And there it is. The problem laid bare. Ironically it reduces to the P and NP one.
all easily varifyable tasks can now be solved with money. this is worth paying attention to. math proofs are verifyable -> math proofs are easy now. you can think of other such tasks: cybersecurity, AI R&D/RSI, killing people, 3d-printing helpful tools, maxxing-out human health, manipulation, self-driving cars, anything that can be checked
all jobs in the future will be those can not be easily verifiably done. if you need a team of people to decide if you have been productive, and those people cant be automated, you're in luck.
I don't really like these articles, because they seem extremely hard to verify. OpenAI has published a lot of stuff in the past where, upon close inspection, what they're saying is technically true but a lot less interesting or impressive than the headline. Except by the time anyone looks into it, the hype has moved on. It seems like there's maybe a thousand people in the world that can even say if this is good or not?
Unrelated to the accomplishment or proof itself, but it's interesting how much of the prompt, even in this latest-and-greatest model, is spent essentially telling the model to actually solve the problem. Things like "Reject status reports, vague optimism, and claims that an unproved global compatibility statement is 'routine'."
Also a lot prompt spent feeding it strategies, which feel like they should/will eventually be deduced by the model itself, not explicitly stated. That's not to take away from the outcome in any way; rather, it feels sort of like when you would prompt GPT 4, "think through your answer step by step," as a sort of proto-chain of thought.