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

101–110 of 467 posts

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

#101

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…

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

Unfortunately in my experience that's not really the case. For me, very often GPT 5.5 (which was a good deal better than Opus at this kind of task) would just get stuck for long periods when working in a logic like Iris. It wouldn't necessarily outright prove nonsense, but it would vastly overclaim what it had proved and failed to get anywhere without a lot of hinting. 5.6 is hopefully a lot better about this.

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

#102

Post by [deleted] »

Jweb_Guru wrote: post #77
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?

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…

[deleted]

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

#103

Post by hellohello2 »

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…

This feels mistaken; we develop abstract objects i.e. graphs based on real-world utility or whatever. As we try to improve our understanding of graphs, we value proofs that help us do so, or help other fields of mathematics. We assign 0 value to random proofs about stuff no one cares about... This conjecture had value, simply because some people found it interesting. It is not really different from music, in a sense.

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

#104

Post by lubujackson »

jvanderbot wrote: post #55
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…

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

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

#105

Post by dwohnitmok »

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…

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

This isn't true using the level of originality you're implying with your software examples.

Technically speaking, many novel mathematics proofs are written all the time (quite a few textbook exercises are actually technically novel problems that have never been posed before they were written in a textbook!) that get absolutely no fanfare. Overwhelmingly though they are not very original or difficult and really just required a fairly routine combination of different pre-existing techniques, even if technically speaking that combination didn't exist before. Those textbook problems are hence easy and therefore not given much public attention even if they are technically novel problems.

Indeed over the course of developing a new mathematical result, many many novel results are glossed over to the extent that even their proofs are left out ("as an exercise for the reader") because they are fairly trivial.

This is true for the overwhelming majority of new software as well. A new CRUD program may, technically speaking, be novel, but it's almost certainly just a routine combination of different pre-existing things.

Mathematics open problems that are actually named are generally problems that have resisted the low hanging fruit of the most obvious combinations of pre-existing problems. When those are solved they are a big deal precisely because they usually require some novelty!

Similarly in software, if someone were to create a new kind of database that solves a variety of new classes of problems that current databases fail to solve that would be a big deal! Truly novel software is also perceived as a big deal. Software that is, technically speaking new, but doesn't actually stray far from a fairly obvious remix of pre-existing techniques, isn't really celebrated.

In both software and mathematics, the intuitive benchmark is if other practitioners in the field look at the result and would say "Wow! How did you do that?" Professional software developers generally don't look at, e.g. a new blogging platform, and boggle at "Wow! How did they make that?!!"

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

#106

Post by varjag »

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.

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

#107

Post by prideout »

scrlk wrote: post #82
simianwords wrote: post #54

what's the difference between Sol Ultra and Sol pro? is pro a thing of the past now

Ultra = parallel subagents with max reasoning Pro = test-time compute (best of N responses)

Confused about how to access Ultra; I don't see it in on their plans page.

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

#108

Post by greenavocado »

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…

I use GPT 5.6 as default and subtask agent and Fable as Advisor with Oh My Pi harness

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

#109

Post by varjag »

ComplexSystems wrote: post #63
emil-lp wrote: post #27

Earlier quoted context omitted.

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.

How many tokens would it cost to write some library functions to fill in the gaps?

You could try solving that in Lean perhaps

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

#110

Post by nilkn »

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.

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