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

61–70 of 467 posts

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

#61

Post by madaxe_again »

andai wrote: post #38
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…

>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’m a physicist, so I’m biased, but my experience of pure maths was about the same. We had to do it, but at no point was any utility actually demonstrated - that was left to the physics professors. It was all just “look at this thing I can do with these symbols” without any actual tangible relationship to anything.

Then again, I remember how we were taught calculus at high school - we were taught how to mechanistically integrate and derive everything under the sun. At no point did anyone think to explain that we were measuring the areas under curves, or their rates of change - it was all just “memorise this operation”. Again it was left to the physics teachers to explain why this was useful, and what we were actually doing.

Poor teaching, if you ask me, and it more often than not left me retrospectively wondering if said mathematicians had actually understood any of what they did, or if they just had little blind symbol manipulation Turing machines in their heads.

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

#62

Post by throw310822 »

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…

> seems that it is exploiting a clever trick that somehow all the experts missed.

Exactly, "clever". Isn't that the whole point?

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

#63

Post by ComplexSystems »

emil-lp wrote: post #27
azaras wrote: post #19

It did not use Lean or other proof assistant?

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?

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

#64

Post by charcircuit »

odo1242 wrote: post #33
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.

Most likely they wrote the proof in Lean and had it verified by a computer

The prompt does not mention Lean.

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

#65

Post by stymaar »

andai wrote: post #38
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…

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

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

#66

Post by [deleted] »

madaxe_again wrote: post #61
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’m a physicist, so I’m biased, but my experience of pure maths was about the same. We had to do it, but at no point was any utility actually demonstrated - that was left to the physics professors. It was all just “look at this thing I can do with these symbols” without any actual tangible relationship to anything. Then again, I remember how we were taught calculus at high school - we were taught how to mechanistical…

[deleted]

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

#67

Post by dooglius »

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…

I wonder if in each case they had parallel sessions, one trying to prove, one trying to find a counterexample

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

#68

Post by therobots927 »

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?

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

#69

Post by _the_inflator »

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…

Wow, you couldn't be more wrong here.

Math is something humans invented and is a model, nothing else. There is no logic per se, but a model that works quite well for us.

I studied Math and CS as a very highly gifted and quickly found out, there is no beauty of Mathematical Logic, only humans approval of what they deem most accurate.

A good example is set theory. Cantor was not openly welcomed after he introduced his "theory" to others. In fact, he was received quite some pushback and hostility - this doesn't sound like someone received love the mathematical logic's way.

In fact, the story of Cantor is really a tragic one. He left math for quite some time, due to the pushback.

Only later humans accepted his theory and found it useful. Well, well, what is Mathematical Logic and what not is after all just broad consensus by humans.

And if you go deeper, you will hear more of these stories. Math is anything else but logic. Proofs are religious things, often so complicated, they are simply accepted as "approved by a committee". Many profs cannot really explain simple proofs, they refer to the textbook.

This doesn't sound like romance nor easily reproducible logic.

After all, we deal with human beings.

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

#70

Post by therobots927 »

emil-lp wrote: post #15
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?

The prompt was released, but not the cost of the result.

And not how many times it was prompted before it returned a working solution.

Or how many prior variants of this prompt were tried.

Or if proof checking software was used to hone in on the final winning prompt / LLM output.

Post reply on HN