Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

cdn.openai.com

Post reply on HN
Print view View original

201–210 of 467 posts

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

#201

Post by qarl2 »

Garlef wrote: post #196
qarl2 wrote: post #193

Earlier quoted context omitted.

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

> a human mathematician would aspire to Some do. But there's also the notion that a clever trick is a bad explanation.

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?

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

#202

Post by pixel_popping »

npinsker wrote: post #85
WhitneyLand wrote: post #75

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

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.

What are you even talking about? The last few years, AI has made an insanely big jump in capabilities, performance, accuracy. It destroyed the carrier of a ton of writers and can generate images that are good enough to bamboozle people into thinking it's human made, that sounds like an insanely big leap to me, and yes it can be very creative and in music as well, I would bet it beats already 90% of musicians (most musicians are not that competent).

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

#203

Post by Miraste »

lubujackson wrote: post #126

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…

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.

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

#204

Post by Jweb_Guru »

therobots927 wrote: post #100
Jweb_Guru wrote: post #92

Earlier quoted context omitted.

I absolutely think that with the rise of LLM generated theorems we need mechanization more than ever, yeah. But I felt that was already pretty important for human proofs, too, and people are just more amenable to the idea now that it doesn't take such heroic effort to formalize things. As far as whether something like Lean could evaluate this proof: sure, if it were mechanized rigorously. But the amount of work that…

I see. So you seem to lean towards it being unlikely they would be able to use lean to evaluate this proof in an automated way…

I'm honestly not familiar enough with how well-developed graph theory is in Lean to be able to say. The paper is mostly using pretty old results, so it's mostly a matter of whether that stuff has already been formalized or not. Like anything else in software (and Lean proofs are very much software) a lot of it's about infrastructure. It wasn't so long ago that no area of mathematics outside of type theory and formal verification was really built up enough to do "serious" math -- that's changed a lot within the last few years.

What I'm more saying is that we're a ways away from being able to straightforwardly go from an LLM having a paper proof to having that proof formalized in Lean in the general case. Not so much because it's hard for LLMs, more just because it's hard in general unless all that background work has already been done. As more and more of foundational mathematics gets mechanized, it will be easier and easier to check your work in Lean while you work on the proof. For example, AFAIK unit distance has already been mechanized (though the quality of the mechanization effort sounds not great, it still greatly increases our assurance in the proof's correctness).

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

#205

Post by paulpauper »

stymaar wrote: post #65
andai wrote: post #38

Earlier quoted context omitted.

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

As a friend of mine who also happens to be a math professor once said: mathematicians are like sculptors who marvel about the beauty of their creation, and are kind of disgusted when a physicist comes nearby and says “that's a cool hammer you got there, may I borrow it?”.

I would be flattered , but that is just me

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

#206

Post by jackphilson »

varjag wrote: post #146
UltraSane wrote: post #139

Earlier quoted context omitted.

If it was in Lean anyone could verify it instantly. That is the huge advantage of it. Manual math Proof verification labor might be the most limited resource ever.

How does it matter if it Lean verified or a human verified proof if you comprehend neither? There can't be too many people working in that corner of graph theory, and I expect the result to them being eminently straightforward.

One requires you to trust a human and the other requires you to trust mathematics.

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

#207

Post by varjag »

jackphilson wrote: post #206
varjag wrote: post #146

Earlier quoted context omitted.

How does it matter if it Lean verified or a human verified proof if you comprehend neither? There can't be too many people working in that corner of graph theory, and I expect the result to them being eminently straightforward.

One requires you to trust a human and the other requires you to trust mathematics.

Let me simplify it for the sake of argument. Imagine I am unable to follow a middle school proof of Pythagoras. How does it matter if I trust anyone beyond that? What possible contribution can I build on top of that?

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

#208

Post by ak_111 »

qarl2 wrote: post #193
ak_111 wrote: post #26

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 "theo…

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

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.

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

#209

Post by BeetleB »

arrowsmith wrote: post #145
BeetleB wrote: post #58

Earlier quoted context omitted.

> I complained in the group chat, that our didactic materials, specifically tasked with providing motivation and concrete examples, did not contain a single application, of this most richly applied field. > I was promptly pilloried, and shunned. Heh. In my day I may have participated in the pillorying. I do think that there is value/merit in professors mentioning real world applications, where they exist . What they'…

Knowledge for its own sake is great, but it's worth noting that many "useless" fields of mathematics turned out to be very practical in the long run. Number theory was long thought to have no practical application, but now it's the backbone of cryptography. Boolean algebra was developed in the 19th century (George Boole died in 1864), decades before it was used to build computers. Those "useless" theorems being prove…

No one is disputing that - not even most mathematicians. They just don't want it to be their job to know the useful applications.

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

#210

Post by qarl2 »

ak_111 wrote: post #208
qarl2 wrote: post #193

Earlier quoted context omitted.

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

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.

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?

Post reply on HN