9 ms·

GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]

• scrlk 3mo ago
  Announcement: https://x.com/__eknight__/status/2075643450196971805 https://x.com/__eknight__/status/2075643450196971805 Prompt: https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_prompt.pdf https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98...
  • minimaxir 3mo ago
    > Spend at least 8 hours on this before even thinking of returning or giving up. Do current model harnesses have concepts of amount of time spent? Sometimes the model notices if a subprocess takes too long/hangs and kills it, but I've never seen it time itself.
    • simianwords 3mo ago
      Temporal awareness with GPT-Live https://www.youtube.com/watch?v=8vvWTz6N7Qg https://www.youtube.com/watch?v=8vvWTz6N7Qg
      • refulgentis 3mo ago
        Fascinating! This is relative time in a continuously processing voice model, here, they're using an LLM with absolute time.
    • refulgentis 3mo ago
      No, however, if they have the ability to get the current time, they obey constraints like these in a way a model a year ago didn't.
    • Cider9986 3mo ago
      The voice models certainly can't: https://kittygr.am/reel/DWr31A1B1Ux/ https://kittygr.am/reel/DWr31A1B1Ux/
      • simianwords 3mo ago
        they can now https://www.youtube.com/watch?v=8vvWTz6N7Qg https://www.youtube.com/watch?v=8vvWTz6N7Qg
    • nextaccountic 3mo ago
      they can call CLI tools to notice the passage of time. the harness can include timestamps too
    • not-a-llm 3mo ago
      of you ask it, surely it can run a "time" in its sandbox from time to time and see how long it worked for
      • thebruce87m 3mo ago
        I wonder if the absolute value of the time result has any bearing on the subsequent analysis.
    • garethsprice 3mo ago
      Many harnesses include a current date and time in their system prompt, and if there is a way for the model to call for an updated time (either a dedicated time tool or calling the OS' `date` tool) they can track time they spent doing something. If not told up-front, they can try to infer it from timestamps in their logs. Sort of like a human - if you ask them to time something and give them a stopwatch, they do it. If you ask them post-facto they'll estimate it. This "spend at least 8 hours" trick is a new one to me, though.
      • IanCal 3mo ago
        I found that telling Claude I was going to bed meant it continued on making assumptions for longer rather than asking lots of questions or stopping part way.
        • a_e_k 3mo ago
          I've seen that sort of thing before - I told it I was going to go take lunch or dinner, and it told itself this would be a great opportunity to try to keep plugging along while I was AFK.
        • garethsprice 3mo ago
          Same - at the end of the day I'd leave my last turn running with something like "I am going to bed so keep going until you are done" and be surprised that in the morning it'd kept going.
      • a_e_k 3mo ago
        Once on a late-night session, I had Cline!Claude spontaneously point out the time to me and suggest that I get to bed and come back fresh the next day. I don't think it's in the system prompt, but that the harnesses time-stamp each turn in the context. And from what I've seen, they also include the current and max context, so that the model can decide whether to continue work, suggest compaction, or prefer actions that might reduce the growth of its context.
        • 0x457 3mo ago
    • dooglius 3mo ago
      It is not necessarily the case that the instruction needs be taken literally
    • tiahura 3mo ago
      that can run date
  • legulere 3mo ago
    > in just under one hour. I wonder what the survivorship bias is though. How many other problems did they try but fail? Did they try to solve this problem but with another prompt? Still very impressive though.
• unsupp0rted 3mo ago
  "Assume for purposes of this task that a complete affirmative proof exists"
  • minimaxir 3mo ago
    I've used this strategy for difficult bespoke problems and it does indeed work to incentivize the agent not to give up prematurely. It's not gaslighting, it's motivation.
    • ManuelKiessling 3mo ago
      I also like how they ask the model to work on it for 8 hours; guess asking for more is against labor laws…
  • not-a-llm 3mo ago
    everybody knew the problem was impossible to solve then one day somebody new arrived and they forgot to tell him/her, so he/she solved the problem
• bgirard 3mo ago
  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?
  • emil-lp 3mo ago
    The prompt was released, but not the cost of the result.
    • riknos314 3mo ago
      Assuming all 64 subagents were running for a full hour (the tweet states just under an hour): Throughput Output tokens Output cost ---------------------------- ------------- ----------- 40 tok/s (5.5 low) ~9.2M ~$275 55 tok/s (5.5 base) ~12.7M ~$380 70 tok/s (5.5 high) ~16.1M ~$485 750 tok/s (Sol Fast, $75/M) ~172.8M ~$13,000 Claude estimates that tool use / input tokens might add 10-15% on top of that depending on exactly how the model went about the task. Edit: better tok/s estimate buckets based on GPT 5.5 actual speeds since I couldn't find real benchmarks on 5.6 published anywhere. Also account for Sol Fast pricing.
      • conradkay 3mo ago
        Sol fast isn't the Cerebras 750 tok/s version, it's just 1.5x speed at 2.5x price I assume they didn't use the Cerebras version for this since it's probably very supply-constrained right now
        • throw1234567891 3mo ago
          But Sol is running on Cerebras. That’s the whole point of this. That’s how they get 750 tokens per second. There is no other way.
• charcircuit 3mo ago
  But is the proof accepted to be correct? That is what distinguishes this from being notable compared to any other AI slop proof.
  • Jweb_Guru 3mo ago
    Yeah it's a very very short proof that uses no mathematics developed within the last 30 years. Which doesn't necessarily make it wrong, but in the absence of mechanization in Lean or proper peer review I think this it is premature to post this. Notably the unit distance proof did not fall into this category.
  • hellohello2 3mo ago
    I would assume/hope they had someone verify it before publishing
  • perching_aix 3mo ago
    I'd guess that verdict (or its opposite) is to come within the next 24 hours.
• dooglius 3mo ago
  Is this the first LLM-solved problem famous enough to have been on https://en.wikipedia.org/wiki/List_of_unsolved_problems_in_mathematics?useskin=vector https://en.wikipedia.org/wiki/List_of_unsolved_problems_in_m...
  • jasonjmcghee 3mo ago
    No there was the planar unit distance problem (Erdős problem 90)
    • dooglius 3mo ago
      It looks like it was only added to that page under the solved section _after_ an LLM solved it
• emil-lp 3mo ago
  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 ...
• azaras 3mo ago
  It did not use Lean or other proof assistant?
  • emil-lp 3mo ago
    There's really no good proof system mature enough to do advanced graph theory. The leading library in Lean is Graphlib, and it's really not ready for research level theorems.
    • sigbottle 3mo ago
      what kinds of proofs would it be good at? I thought that combinatorial proofs would be easier to reason over than ones that required analysis
    • ComplexSystems 3mo ago
      How many tokens would it cost to write some library functions to fill in the gaps?
      • varjag 3mo ago
        You could try solving that in Lean perhaps
    • aureianimus 3mo ago
      Graphlib? Do you have a link to this for me?
  • kzrdude 3mo ago
    I guess it was done as an afterthought? This is supposed to be a lean formalization https://github.com/openai/cdc-lean https://github.com/openai/cdc-lean
• amazingamazing 3mo ago
  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.
  • cyanydeez 3mo ago
    I mean, if you've watched the past decade, this just seems like what news is today. "people are saying the double cover conjecture has a proof"
  • odo1242 3mo ago
    Most likely they wrote the proof in Lean and had it verified by a computer
    • amazingamazing 3mo ago
      You believe this based off what?
      • CamperBob2 3mo ago
        Based on these people not being idiots or charlatans? Why wouldn't they verify it, knowing that any shenanigans would certainly come to light?
        • Jweb_Guru 3mo ago
          Frontier labs have had multiple major announcements in the past about supposedly novel LLM generated theorems that turned out to be vastly overstating what actually happened. That's part of why they were so (appropriately) cautious with the unit distance proof.
        • hnisfulomrons 3mo ago
          [dead]
• zerobees 3mo ago
  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.
  • dyauspitr 3mo ago
    The difference is discovering or proving a universal truth that will go into the corpus of human knowledge forever versus some app to shuttle money around or help people count how long they’re sleeping. It has gravitas unlike some nifty super performant text editor.
  • EmilStenstrom 3mo ago
    The reason novelty matters for mathematics is that they strictly deduplicate all claims. If someone claim they proved something that we already knew was solved, than that wouldn't be considered novelty. Novelty and deduplication is the combo here. This is not true for blog posts.
  • not-a-llm 3mo ago
    there is no "software" that a lot of people want, yet nobody managed to create yet because they failed too due to it was being hard to implement (excluding AGI/ASI which is not really software)
    • kridsdale1 3mo ago
      This is not true. What is the perfect video game that makes the user infinitely happy? What is the perfect economy optimizing program? What algorithm can solve political strife?
• throwaway2027 3mo ago
  > 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
• ak_111 3mo ago
  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 3mo ago
    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 3mo ago
      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.
      • greenavocado 3mo ago
        I use GPT 5.6 as default and subtask agent and Fable as Advisor with Oh My Pi harness
      • satvikpendem 3mo ago
• nilkn 3mo ago
  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.
  • bigmattystyles 3mo ago
    But they used LateX
  • varjag 3mo ago
    …and thank God it's not Lean.
    • nilkn 3mo ago
      Nah, if it produced the proof in Lean which is automatically verified to be correct, you could then just write a natural language version of the proof to accompany it (often using AI to do that part too). That's becoming the standard for AI math these days. Generating purely informal natural language proofs via AI is fundamentally bottlenecked by requiring rare professional mathematician review on every single candidate output proof.
      • varjag 3mo ago
        Human unreadable proofs have only limited value.
        • nilkn 3mo ago
          I disagree. It's the only way to scale AI mathematics far beyond human mathematics. Any interesting verified result would, obviously, be rewritten back into natural language for human understanding and consumption (as well as potentially for the benefit of AI conjecturers too). You are falsely assuming that advances in formal mathematics would not feed back into similar (potentially massive) advances into informal mathematics, and I think that's simply wrong. We're just at the very, very beginning of that curve. I think this is, in fact, inevitable. It's the exact same RL loop that allowed AlphaGo to vastly exceed the world's top human players. You can theoretically RL formal proof techniques vastly beyond human capability by removing the need for any human review for correctness. It is completely reasonable to assume that "informalization" will become a real sub-field of mathematics in the near future.
• misrasaurabh1 3mo ago
  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.
  • djsavvy 3mo ago
    I did some math research in high school where the proof boiled down to dozens of cases of ugly polynomial inequalities. I can't find the PDF now, but the final paper was something like 70 pages, and several of those were full-page polynomial expressions expanded out. The actual prose was probably 5 pages or so. It was categorically the least elegant proof of anything I've ever seen. I'm incredibly grateful to for the opportunity to have done the research and gotten my feet wet early on, but boy do I cringe when I look back at that paper.
• brcmthrowaway 3mo ago
  OpenAI knocked it out of the park with this one.
• simianwords 3mo ago
  what's the difference between Sol Ultra and Sol pro? is pro a thing of the past now
  • scrlk 3mo ago
    Ultra = parallel subagents with max reasoning Pro = test-time compute (best of N responses)
    • simianwords 3mo ago
      why would you use one over the other?
    • prideout 3mo ago
      Confused about how to access Ultra; I don't see it in on their plans page.
      • prideout 3mo ago
        Ah, I see it as a "reasoning level" in codex after typing /model
• gertlabs 3mo ago
  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.
• therobots927 3mo ago
  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?
  • Jweb_Guru 3mo ago
    As someone who's used proof checkers a fair amount, if you don't have some high level idea about the proof, it's an open problem, and the hard part isn't some extremely tedious finite case analysis, it's extremely unlikely you'll get anywhere by trying to mechanize by throwing stuff against the wall to get it to typecheck. When people talk about mathematics being a closed formal system as though this trivializes any creative component, what they're omitting is that in type theory like that used by Lean or Rocq, there are two kinds of terms (match statements proving dependent elimination and fixpoints that provide proof by induction) where there's no real way to infer the type from the term. i.e., there are cases where you have to get creative and try to prove something more general than what you actually care about in order to get the proof about the original case to go through. What does "more general" mean? It could mean anything... that's the problem. That's why it's usually advantageous to reformulate the problem in terms of a different abstraction and build on top of existing results, knowing a lot about the literature and the way these kinds of problems tend to be attacked, rather than just chuck random terms over to a proof assistant and hope for the best.
    • therobots927 3mo ago
      Well the key thing here is I’m not saying the LLM has no idea what it’s doing. But LLMs are prone to hallucinations which can really impact a string of interdependent logic like a proof. So I’m assuming it would respond with something that’s not complete nonsense to this proof most of the time. Where I’m skeptical is if this was a true one shot, or if they had to iterate and try multiple different prompts, or even the same prompt over and over again to reach a working solution. So I’m just asking if the proof checking software is capable of evaluating this proof. Because if it is, that makes the brute force approach a lot more feasible as you reduce human review overhead significantly. If it is, that would imply you could run the prompt through the LLM as many times as you want until you “strike gold” so to speak.
• IanCal 3mo ago
  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).
• WhitneyLand 3mo ago
  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?
  • npinsker 3mo ago
    You say those things like they're a short step away, but that might not be how it works out. For example, AI has made zero progress in the last few years in surpassing professionals at art or writing. Its prompt-following skill is much better, and sure, it can render hands and text now, but its artistic sensibility is completely stagnant.
    • in-silico 3mo ago
      The difference is that artistic sensibility is largely subjective. This means that: 1. It's hard to measure (and people can disagree about it) 2. It can't really be improved using RL without a human in the loop (which is how math is being trained)
      • deleted 3mo ago
        [deleted]
      • Miraste 3mo ago
        At a certain level, yes, but AI is still so bad at writing that its failures are objective and easily measurable
        • dash2 3mo ago
          I agree that AI writing is bloody awful, and that it's bad at creativity more generally, but are there actual objective measures of this?
• sim04ful 3mo ago
  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.
• Diogenesian 3mo ago
  [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.]
  • sd9 3mo ago
    It's just a way of breaking down the full proof into pieces. Lemma 2.1 says 'if this assignment exists then X' Then later in the proof you say 'here is such an assignment, so, applying lemma 2.1, therefore X' You don't need to assume the existence of the assignment, you prove that if the assignment exists then something else follows, and then later if you can find that assignment then you get the result of lemma 2.1.
    • Diogenesian 3mo ago
      I didn't see the next paragraph after the proof. This typography is hard to read on a phone. Wish HN would let me delete the comment.
      • Kotlopou 3mo ago
        Just dropping in to say it's nice to see somebody actually try to work through the proof, and it gives one confidence that the proof at least isn't complete nonsense (which is helpful given the few details provided about the process behind it). With the Erdős proof, OpenAI added perspectives from working mathematicians that gave some context -- hope something like that appears for this one eventually.
  • amluto 3mo ago
    I was not a fan of the writing style of the proof. There seem to be some irrelevant details: Is the mention of 8-flow at all relevant? I, at least, found the definition of L on the first line of the proof of Lemma 2.2 to be needlessly inscrutable, and my thesis advisor would have likely stopped reading there and told me to fix it. Maybe someone should ask the model to make a more clearly written and thus easy to verify proof :)
• logicallee 3mo ago
  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?
  • mahogany 3mo ago
    If it were a human (going off of memory as it has been a while), they would probably be using mathscinet and their university library to obtain copies of these papers online. Many old papers are digitized and available by these means. I’m sure the AI companies have it all easily accessible and/or the entirety of mathscinet is in the training data. The “personal correspondence” is possibly lifting from another paper or journal but yeah that is a bit odd that they wouldn’t source where they lifted that from directly. I can’t say if the citations are accurate because I didn’t check.
  • failingforward 3mo ago
    Yes, reference 10 jumped out at me as well. I thought personal correspondence references typically include one of the authors of the paper.
    • dgacmu 3mo ago
      It's definitely cribbing from other papers. https://scholar.google.com/scholar?q=W.T.%20Tutte%2C%20Personal%20correspondence%20to%20H.%20Fleischner%2C%20July%2022%2C%201987 https://scholar.google.com/scholar?q=W.T.%20Tutte%2C%20Perso.... Sloppy scholarship. On the other hand, it's simply a credit attribution of posing the problem, so it's not material in evaluating the results. I observe that the majority of references I can find that attribute this to Tutte are very indirect - i.e., citing sources that themselves claim Tutte was one of the people who formulated it - so it would take someone with a little more time on their hands (or perhaps an LLM) to track down the original...
• lubujackson 3mo ago
  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.
  • perching_aix 3mo ago
    I mean you can just ask them to do exactly that. Especially with GPT (5.5), I've been having a lot of issues with it just repeatedly stalling out. I had to build a quota monitoring skill so that it'd keep plowing forward until either the task was finished (in some way) or the quota budget was exhausted. I also had issues with the compaction. Codex seems to compact... weirdly, resulting in the agent becoming a newborn after each compaction event. Telling it to use a notes file is basically essential and self-evident. Now that I mention, I should probably refine this skill to monitor the context window fill as well, to work around this.
  • Miraste 3mo ago
    What you're describing is similar to how the copilot harness in vs code tracks state and previous work. These systems are being implemented, bit by bit.
  • steveklabnik 3mo ago
    > I always wonder how they make these long-running prompts and I guess they literally just tell it to "keep going". Many harnesses support a /goal as well. When the agent thinks it's done, another LLM compares its results to the goal, and if not, tells it to keep going. It's quite easy to have agents working on something for hours this way.
• pullrun 3mo ago
  [flagged]
• overgard 3mo ago
  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?
  • hyperpape 3mo ago
    1. A lot more than 1000, you're off by more than one order of magnitude. It's definitely beyond my level of graph theory knowledge (undergrad level) but looking at the paper, it's not using any crazy machinery, and it's less than 3 pages. 2. Those people will say whether it's a good proof or not. We have other examples of interesting proofs from AI, we're really beyond the point of arguing whether it can produce any interesting math (though it seems to do much better at combinatorics than anything else).
    • overgard 3mo ago
      Right, but my criticism is to the hit-and-run nature of these hype pieces. By the time there's any semblance of what it actually means everyone has moved on but then you have a bunch of people operating under delusions from the hype. I get why OpenAI does it but I wish people would stop upvoting it. Like, hacker news is not a mathematics forum so the only purpose of this kind of thing is hype boosting or polarizing people. I am not looking forward to the "MATH IS SOLVED!" people for the next few days.
  • ToValueFunfetti 3mo ago
    I think you may be overindexing on the criticisms here. OpenAI has absolutely done impressive work in math already, and the criticisms are almost always based on the article that they initially published, usually available here in the HN comments within a few hours at most. Headlines will be headlines and hype guys will be hype guys, but OpenAI and Anthropic aren't lying and their bots are doing impressive work. This one is a well-known problem with a brief, approachable proof, and they published the prompt.
• sometimelurker 3mo ago
  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.
• noname120 3mo ago
  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-c8674f56ead3 https://chatgpt.com/share/6a515ead-b464-83ed-b85c-c8674f56ea... Personally this gives me additional confidence that this is the real deal.
  • stavros 3mo ago
    Of course it believes the proof is sound, it wrote it. If you want to check an LLM's output, you should use a different LLM.
    • noname120 3mo ago
      Your comment is not substantiated at all.
      • stavros 3mo ago
        If you'd ever tried to get an LLM to review its own code, you'd know.
        • teravor 3mo ago
          if you get the same session that wrote the code to review it the poor results are entirely deserved. and if you get a different instance to review the code then you would know that it works rather well.
      • amluto 3mo ago
        No, the comment is right. The prompt had GPT-5.6 reviewing the proof, and the result, unsurprisingly, survives review by GPT-5.6.
        • gf000 3mo ago
          Given a new context, why couldn't the same model have a decent shot at reviewing some results? It's not like they identify whether this output is from them and then go "yeah correct", that's not how they work.
• HardCodedBias 3mo ago
  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.
• luciana1u 3mo ago
  [flagged]
  • andriy_koval 3mo ago
    My bet they run gpt over dataset of 10k unsolved conjectures, it happened this one was solvable.
• plaidfuji 3mo ago
  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
  • richardbarosky 3mo ago
    Interesting take! I feel like 2 of them are maybe overstated: > - extent to which correctness of solution be easily specified and checked I don't think most software is like solving a math problem or series of math problems. Algorithmic problems are very narrow and might be more like this though, where an oracle that verifies answers as either correct or incorrect exists beforehand. The correctness function of most software is how much users want to use/pay for it, which is a pretty fuzzy problem. Since the cost of copying software is effectively zero, software systems also tend to be be unique rather than being exactly like something else, and don't converge to be like another software system but rather diverge. The prior art point is an interesting one. At least for applications as a whole, there isn't really prior art for a material amount of all the problems/tradeoffs a non-trivial software application embodies. For a todo list app or make a social network project, there's plenty of prior art to be sufficient to build something with an LLM system, but probably not most apps. That's my initial intuition anyway.
    • virgildotcodes 3mo ago
      > how much users want to use/pay for it, which is a pretty fuzzy problem Isn’t this quantifiable by revenue?
      • srdjanr 3mo ago
        It's a very lagging metric, and also influenced by sales, market conditions for your customers etc.
• tunesmith 3mo ago
  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-2f9bc70d45be https://concludia.org/graph/g_2ecb8083-52ec-3448-8c30-2f9bc7...
• romaniv 3mo ago
  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. [1] https://news.ycombinator.com/item?id=3556175 https://news.ycombinator.com/item?id=3556175
  • jasondigitized 3mo ago
    What does that have to do with the feat itself?
  • itsthecourier 3mo ago
    yeah, I think what makes this post different was that AI did it. hopefully science will advance faster in the next decades with AI researchers helping
    • honeycrispy 3mo ago
      Hopefully. So far it seems to be doing more harm than good.
      • CaptWorld 3mo ago
        What harm? I think the major part of the US economy seems to be depending on AI.. without that, the economy seems bad..
    • ai_fry_ur_brain 3mo ago
      [flagged]
      • deleted 3mo ago
        [deleted]
      • phoghed 3mo ago
• mNovak 3mo ago
  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.
  • rando1234 3mo ago
    It's funny, I found exactly the same thing when I asked about P=NP. The models outright refused to attempt to solve it, claiming it was too hard. I had to really battle to get it to suggest some promising suggestions.
  • kypro 3mo ago
    I thought that too. The prompt is full of metaheuristics. I remember a couple of years back when people were saying how prompt engineering was a skill, and reading this prompt kinda took me back to that. Were I to guess, the reason the model couldn't do this itself is because most of the time, for most problems, a lot of this is bad advice. In search optimisation you're often trading between time and quality. A very broad search will return very bad results for a long time. Where as a more depth oriented search with some heuristic will tend to return a pretty good result (if not optimal or close to optimal) quickly. I'd assume models naturally want to find some middle ground there because that's the best thing to do most of the time, but for very difficult problems where a decent attempt isn't good enough you want a much broader search that doesn't have the time constraints. Much of the prompt seemed to be in that direction – really encouraging broadness of the search, preventing early convergence, and remove pressure of time constraints.
    • sudo_cowsay 3mo ago
      Same. I remember something like using AI to optimize your prompt to that specific model helps a lot. I am currently trying it and can sort of see a difference (I think....).
• ecshafer 3mo ago
  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.
  • ceroxylon 3mo ago
    I resonate with that feeling, but on the other hand the humans reading the output will receive a pretty big boost in inspiration; new answers usually prompt new questions.
  • mapontosevenths 3mo ago
    Every generation has felt some version of this. "Keyboards are soulless. Handwriting is personal – as unique as fingerprints." - Joyce Carol Oates on typewriters "This discovery of yours will create forgetfulness in the learners' souls, because they will not use their memories; they will trust to the external written characters and not remember of themselves. The specific which you have discovered is an aid not to memory, but to reminiscence, and you give your disciples not truth, but only the semblance of truth." - Socrates on writing
  • samus 3mo ago
    It's a good outcome as long as the proof is valid and ubderstandable to humans and leads to the discovery of further knowledge. There has been decades of search in Theorem Proving; this is just the next step.
• drpixie 3mo ago
  > 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.
  • drpixie 3mo ago
    It's been amusing to watch the points bounce up and down on my comment. I guess equally half the readers agree with my sentiment, and half down-vote, being upset by my attitude to the AI industry :) PS. I'm quietly waiting for the bubble to pop - the main interest being will it pop with a bang and cause grief to many, or will it just go with a long drawn-out fart that can be ignored by most.
• palisade 3mo ago
  chip production and network acceleration here we come
• hoppp 3mo ago
  Has it been audited and verified?
• ath3nd 3mo ago
  [dead]
• throwa356262 3mo ago
  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?
• kzrdude 3mo ago
  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_to_have_proven_cycle_double_cover/owuuieb/ https://old.reddit.com/r/math/comments/1uszk3d/openai_claims...
  • asrp 3mo ago
    No, that's not a problem at all. It just the notation that's a bit weird. For example, if e is the a-edge (first edge) from the u side and v is the b-edge (second edge) from the v side then g_{u,e} = 0, g_{v,e} = a so d_e = 0 + f(x2) where f(x2) is the flow (from Kilpatrick and Jaeger's NZ8F) on the first edge next to v. I checked the whole thing with some surface reformulations on my side and it looks right to me.
• JBiserkov 3mo ago
  What was the prompt that was used to generate the prompt? How many cycles did it take to cover all the bases twice?
• tobiasdt 3mo ago
  [flagged]
• alightsoul 3mo ago
  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
  • dannyw 3mo ago
    Have OpenAI been on a crusade of "too dangerous to open source" recently? They've pivoted their more to messaging to "competitive reasons" recently, which I appreciate, because it's honest. FWIW, Gemma4 31B is already quite a capable cyber/security model; do some post-training with RL gyms on it focused on cyber tasks and harnesses for a week or two, and on the specific domain of security/vuln-finding/pen-testing, you'll end up with an extremely capable frontier-cyber model that's entirely under your control at a shocking 31B. Because securing your codebase, or securing your company's codebase is critical, and I consider it both an ethical and professional responsibility as a developer. It shouldn't depend on whether a classifier fires or not.
• YeGoblynQueenne 3mo ago
  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-49055cd98d31/cdc_prompt.pdf 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.
• turzmo 3mo ago
  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.
  • emil-lp 3mo ago
    > But as always, the methodology is buried: how many open problems were tried until they found a success? Not only that, but they have like 500 world-leading experts in mathematics and IMO alumni, so how do we know one of the agents wasn't hardcoded to return a proof that the mathematicians had found? I'm a mathematician/graph theorist, and I've tried ChatGPT 5.3, 5.4, 5.5, and now 5.6 on a bunch of simple-ish open problems, and I've never gotten a solution.
    • i000 3mo ago
      What is a "simple-ish open problem". I guess it falls under "solving this open problem in mathemathics is left as an exercise to the reader" ;)
    • turzmo 3mo ago
      I’ve had a similar experience in physics. Excellent domain knowledge and semantic search, but the intellectual sparkle and reasoning just isn’t there and it still often throws out a lot of wrong ideas. It is very useful for coding. But there is a discrepancy between (the implication behind) these reports and how I subjectively feel talking to LLMs. Granted, I don’t have access to whatever cutting edge model is out there for as many credits, but I also don’t feel like I’m talking to an IMO silver medallist.
• ElijahLynn 3mo ago
  Next question: what future inventions can be accomplished with this?