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

131–140 of 467 posts

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

#131

Post by Diogenesian »

sd9 wrote: post #118
Diogenesian wrote: post #99

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

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.

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.

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

#132

Post by arm32 »

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…

So I suppose the value is that something like this gets used as a primitive to solve something that actually has impact. Ah, mathematics, never change!

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

#133

Post by desertrider12 »

therobots927 wrote: post #68

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?

On the last Dwarkesh podcast with 3blue1brown, one of them mentioned that frontier models are now able to work through a whole proof in natural language, just like a human mathematician would. But when they first solved IMO problems in 2024, they relied more on Lean to catch hallucinations.

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

#134

Post by [deleted] »

BeetleB wrote: post #58
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…

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

[deleted]

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

#135

Post by ToValueFunfetti »

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.

I think, and I may be totally off base, that the labs are specifically avoiding art and (non-technical) writing as an endpoint. It's bad PR for them- it calls attention to the copyright question and threatens the 'human flourishing' kind of jobs- and there's no money in it because people prefer art to be human made and there's hardly any money in that anyway.

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

#136

Post by Kotlopou »

Diogenesian wrote: post #131
sd9 wrote: post #118

Earlier quoted context omitted.

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.

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.

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.

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

#137

Post by varjag »

UltraSane wrote: post #125
varjag wrote: post #106

Earlier quoted context omitted.

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

It's not a long proof (it's not in Lean after all) so easy enough to comb through for a domain expert.

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

#138

Post by mahogany »

logicallee wrote: post #111

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

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.

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

#139

Post by UltraSane »

varjag wrote: post #137
UltraSane wrote: post #125

Earlier quoted context omitted.

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

It's not a long proof (it's not in Lean after all) so easy enough to comb through for a domain expert.

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.

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

#140

Post by CSMastermind »

not-a-llm wrote: post #25
bgirard wrote: post #9

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?

pretty sure already millions of dollars (in inference costs) were already thrown at the Riehmann hypothesis as the models get stronger, larger amounts will be thrown at it imagine paying "just $1 bil" to go down in history as the company who's model solved the hardest/most famous open problem in mathematics. imagine the worldwide press headlines. as they say, the Riehmann Hypothesis is the hardest way to earn a milli…

I mean if there's something I'd bet against being solved by LLMs in my lifetime it's that one. We truly do not have line of sight into what a proof would even look like.
Post reply on HN