OpenAI knocked it out of the park with this one.
GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
31–40 of 467 posts
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#32Is this the first LLM-solved problem famous enough to have been on https://en.wikipedia.org/wiki/List_of_unsolved_problems_in_m...
No there was the planar unit distance problem (Erdős problem 90)
It looks like it was only added to that page under the solved section _after_ an LLM solved it
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#33Good 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.
Most likely they wrote the proof in Lean and had it verified by a computer
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#34"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.
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#35This 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…
The reason novelty matters for mathematics is that they strictly deduplicate all claims. If someone claim they proved something that we already knew was solved, than that wouldn't be considered novelty. Novelty and deduplication is the combo here. This is not true for blog posts.
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#36This 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)
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#37Since 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…
But they used LateX
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#38This 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 fields in the real world. It's "perhaps the most applied branch of mathematics in existence".
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.
(Apparently that particular department was the wrong one, to ask a question like that!)
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#39It'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’m all for it since it’s value directly returned to humanity.
Re: GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf]
#40Good 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.
Most likely they wrote the proof in Lean and had it verified by a computer
You believe this based off what?