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

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

#121

Post by jojva » Fri, Jul 10, 2026, 8:05 PM UTC

zerobees wrote: post #22

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 relea…

Isn't it immediately obvious that solving something that humans have been unable to do for decades or more is the most tangible proof of ASI, or at the very least pretty good AGI?

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

#122

Post by dooglius » Fri, Jul 10, 2026, 8:08 PM UTC

minimaxir wrote: post #3

scrlk wrote: post #2

Announcement: https://x.com/__eknight__/status/2075643450196971805 Prompt: https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98...

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

It is not necessarily the case that the instruction needs be taken literally

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

#123

Post by zerobees » Fri, Jul 10, 2026, 8:08 PM UTC

not-a-llm wrote: post #36

zerobees wrote: post #22

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 relea…

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)

As a person who has a number of relatively niche hobbies, I assure you that this is not true. There's a ton of simple things that can be build and will make an immediate difference in the lives of thousands. Watch the workflow any musician, videographer, machinist, etc - they're full of small, weird inefficiencies that AI hasn't really solved for them.

It's just that you can't build a billion-dollar company around it. No one could go to a VC and say "we're going to be the Uber of focus stacking and dust removal for microscopy" or "we're the Uber of aligning the beats in two audio tracks".

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

#124

Post by a_e_k » Fri, Jul 10, 2026, 8:08 PM UTC

IanCal wrote: post #76

garethsprice wrote: post #51

Earlier quoted context omitted.

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. I…

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.

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.

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

#125

Post by UltraSane » Fri, Jul 10, 2026, 8:08 PM UTC

varjag wrote: post #106

nilkn wrote: post #28

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 ou…

…and thank God it's not Lean.

What a ridiculous thing to say. If it was verified in Lean we could be much more confident the proof is correct.

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

#126

Post by lubujackson » Fri, Jul 10, 2026, 8:09 PM UTC

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.

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

#127

Post by azan_ » Fri, Jul 10, 2026, 8:10 PM UTC

andai wrote: post #38

zerobees wrote: post #22

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 relea…

>mathematics is basically the only scientific discipline that rejected any notion of utility I think this might depend on the department, but I was at a pure math department last year, and struggling with my Linear Algebra textbook (written by the professor, incidentally, who was not a great communicator). I consulted the machines, and learned, to my great delight, that linear algebra is used in like 20 different fie…

Typical pure-math linear algebra course has to cover so much material that there's really no time for applications! That's why applied math is typically separate track.

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

#128

Post by satvikpendem » Fri, Jul 10, 2026, 8:10 PM UTC

lubujackson wrote: post #104

jvanderbot wrote: post #55

Earlier quoted context omitted.

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.

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 ge…

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.

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

#129

Post by QuesnayJr » Fri, Jul 10, 2026, 8:11 PM UTC

zerobees wrote: post #22

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 relea…

It's newsworthy because it's a milestone. It was something no human was able to do (despite trying very hard), but a machine did. Humans have written lots of interesting blog posts.

The idea that mathematics has rejected any notion of utility is absurd. It's not like topics get picked at random. Conjectures like this are interesting because they are a test of our understanding. The problem sounds easy, but apparently was quite hard.

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

#130

Post by QuesnayJr » Fri, Jul 10, 2026, 8:13 PM UTC

andai wrote: post #38

zerobees wrote: post #22

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 relea…

>mathematics is basically the only scientific discipline that rejected any notion of utility I think this might depend on the department, but I was at a pure math department last year, and struggling with my Linear Algebra textbook (written by the professor, incidentally, who was not a great communicator). I consulted the machines, and learned, to my great delight, that linear algebra is used in like 20 different fie…

If it was the students, then students can have things they think are cool or uncool.

If it was the professor, then that would be very embarassing on his or her part.