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

91–100 of 467 posts

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

#91

Post by anp »

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 far from a perfect analogy but I would imagine that people were pretty hyped about the novelty of the first legitimately useful compiled programs where they didn’t have to allocate their own registers. I wonder how long it took for that novelty to wear off?

Or in other words I’d argue novelty is contextual and that these kinds of discoveries’ novelty will eventually wear off too but for right now it’s pretty cool that the “math discovery compiler” works well enough to do this (again imperfect analogy).

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

#92

Post by Jweb_Guru »

therobots927 wrote: post #83
Jweb_Guru wrote: post #77

Earlier quoted context omitted.

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…

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

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 takes to do varies with both subject and complexity of result. In this case, from what other people are saying, the infrastructure for doing graph theory proofs like this isn't as built up as it is for some other areas of mathematics, so it might take a while.

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

#93

Post by esafak »

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…

> What's left?

I think humans will be left to propose new conjectures while machines fill out the proofs. I don't know if there are enough interesting conjectures to go round to build new careers, though.

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

#94

Post by hellohello2 »

amazingamazing wrote: post #20

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.

You seem to be suggesting that it is just as hard to understand an existing proof to a problem, than to solve it yourself? I don't follow your argument at all, what are you trying to say?

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

#95

Post by ManuelKiessling »

minimaxir wrote: post #34
unsupp0rted wrote: post #8

"Assume for purposes of this task that a complete affirmative proof exists"

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 .

I also like how they ask the model to work on it for 8 hours; guess asking for more is against labor laws…

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

#96

Post by dnautics »

BeetleB wrote: post #50
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 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. No, the value is that Erdos's name is attached to it. Lots of mathematicians prove things they don't publish, or their manuscripts get rejected - not because of a flaw in the proof but because no one cares about the theorem they proved. And I'm sure it'll be the case with LLM models…

> No, the value is that Erdos's name is attached to it.

That's unnecessarily reductive. you could have said "most of the value is that erdos' name is attached to it"

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

#98

Post by hnisfulomrons »

CamperBob2 wrote: post #73
amazingamazing wrote: post #40

Earlier quoted context omitted.

You believe this based off what?

Based on these people not being idiots or charlatans? Why wouldn't they verify it, knowing that any shenanigans would certainly come to light?

[dead]

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

#100

Post by therobots927 »

Jweb_Guru wrote: post #92
therobots927 wrote: post #83

Earlier quoted context omitted.

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

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…
Post reply on HN