It did not use Lean or other proof assistant?
I guess it was done as an afterthought? This is supposed to be a lean formalization https://github.com/openai/cdc-lean
GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
391–400 of 467 posts
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#392I 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 no…
You are basically right. The real acceptance of the proof comes when it's accepted to a journal after review.
However, in some sense spreading a proof needs to be done in math - then the community reviews and decides if it is valid.
We can't ignore the timing here though: this is a publicity piece for GPT 5.6!
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#393If 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 alie…
It's hard for me not to think what's the point. I am a very average, even below average person in times of intelligence. What is even my value or reason to be if I know anything I can do, LLMs can do better? What is even my value both on job market and as a human?
Remember that the most valuable human in the world is Elon Musk. What it means to be valuable is to be like Elon Musk. Calibrate your goals accordingly.
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#394Over 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...
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#395Is 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?
As someone who was a research assistant in this field one summer back in college, I spent the day trying to check the proof, or at least the obvious places a mistake would be. It's surprisingly readable, so I guess we'll find out soon.
Lemma 2.2 specifically "feels" new to me. You can get part of the way by duct-taping several papers together (playing along at home: I found Tutte 1954, Bermond–Jackson–Jaeger 1983, Máčajová–Škoviera 2005, Zaslavsky 1982. interestingly, only Tutte appears in the works cited). But it's surprising you'd think to pick those, and surprising it works, because you still need a genuinely novel parity argument at the end. Those steps individually are all pretty simple, knowing to chain that chain together, isn't.
The guess-against the checker paradigm is real (ie AlphaProof), and something like that was probably involved here. But this area of graph theory isn't in mathlib, you need to write the proof checker first, and then you need to know what kind of proof checker you need to write (or just do a brute force search for new proof checkers). Probably how you got this result is have a recursive tree of agents until you divide into small enough subproblems.
At a certain point you need a philosopher to figure out what that "means", ie if you have a big enough tree of small enough subproblems, some of the "magic" so to speak moves out of the proof checkers and into the way the tree got structured.
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#396What was the prompt that was used to generate the prompt?
How many cycles did it take to cover all the bases twice?
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#397Earlier quoted context omitted.
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.
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…
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.
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#398[flagged]
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#399Earlier quoted context omitted.
I think a lot of this has to do with the post-training these models normally get. They are designed to answer basic questions with straightforward and short summary answers. They have the capacity to reason deeply, but they are not biased towards that unless prompted. I think it's because LLMs as they are in 2026 are both highly capable but also parlor tricks. They are not sentient, you just set them up with the cont…
Something I've noticed is that if you run Qwen 3.6 35B-A3B (Q8) with a low temperature of 0.4, and leave default reasoning turned on, it will spend quite a lot of time in reasoning/thinking mode. But often it does figure out how to solve something on its own by correcting itself within its reasoning loop before it outputs the final 'answer'. If you watch the progress of the reasoning in llama-server while it's doing…
You'd have less problems with 27B, btw.
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#400Earlier quoted context omitted.
I think a lot of this has to do with the post-training these models normally get. They are designed to answer basic questions with straightforward and short summary answers. They have the capacity to reason deeply, but they are not biased towards that unless prompted. I think it's because LLMs as they are in 2026 are both highly capable but also parlor tricks. They are not sentient, you just set them up with the cont…
Even Fable hallucinates. I had it tracking down some very obscure Ancient Greek inscriptions and the response just made up a translation/context for one inscription after "looking it up." Now, it was still a very particular thing and I really had to get into the weeds to push it to that point, but who knows how many other gaps, near or far, it will happily skip over just for the sake of coherence. I think this is an…
>Even Fable hallucinates
It’s in the name :)