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

141–150 of 467 posts

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

#141

Post by charcircuit »

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…

>At no point did anyone think to explain that we were measuring the areas under curves, or their rates of change

In my experience you get taught the definition of a derivative of a function at a point is equal to the instantaneous rate of change and that integrals are defined as a Reimann Sum, the sum of the area under the curve. Everything in the class comes from building on top of those definitions.

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

#142

Post by jaggederest »

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 love teaching kids and young adults calculus by socratic method. They get so mad when they figure out you were teaching them math, but they often admit it was pretty fun. Only had the chance to teach like that a few times but it's dynamite when it happens.

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

#144

Post by varjag »

nilkn wrote: post #110
varjag wrote: post #106

Earlier quoted context omitted.

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

Human unreadable proofs have only limited value.

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

#145

Post by arrowsmith »

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

Knowledge for its own sake is great, but it's worth noting that many "useless" fields of mathematics turned out to be very practical in the long run.

Number theory was long thought to have no practical application, but now it's the backbone of cryptography. Boolean algebra was developed in the 19th century (George Boole died in 1864), decades before it was used to build computers.

Those "useless" theorems being proved today may turn out to unlock a world-changing technology centuries from now. When the breakthrough comes we'll be grateful for the people who laid the foundations.

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

#146

Post by varjag »

UltraSane wrote: post #139
varjag wrote: post #137

Earlier quoted context omitted.

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.

How does it matter if it Lean verified or a human verified proof if you comprehend neither?

There can't be too many people working in that corner of graph theory, and I expect the result to them being eminently straightforward.

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

#147

Post by StefanBatory »

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…

It's hard for me not to think what's the point. I am a very average, even below average person in times of intelligence. What is even my value or reason to be if I know anything I can do, LLMs can do better? What is even my value both on job market and as a human?

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

#148

Post by Someone »

torginus wrote: post #79
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 thought linear algebra was pretty much the poster child of applied mathematics - the entire field was invented to represent computations in a regularized form to feed into computers. Well not really, but much like Boolean algebra or the Fourier Transform, it was pretty much a curiosity until computers came along.

> but much like Boolean algebra or the Fourier Transform, it was pretty much a curiosity until computers came along.

https://en.wikipedia.org/wiki/Linear_algebra#History: “Later, Gauss further described the method of elimination, which was initially listed as an advancement in geodesy”

That’s an application of linear algebra in the 19th century.

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

#149

Post by s3p »

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

Hear me out on this one:

For a lot of math departments, that is exactly why they teach this. Education is rooted in application. We have entire careers that depend on certain aspects of mathematics, so most companies gatekeep that career by a degree. The degree requires the class. The student taking the class may not even be old enough to drink alcohol yet, and they can't possibly be expected to know of all the applications. Knowing and not telling them is doing them a disservice.

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

#150

Post by nilkn »

varjag wrote: post #144
nilkn wrote: post #110

Earlier quoted context omitted.

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

Human unreadable proofs have only limited value.

I disagree. It's the only way to scale AI mathematics far beyond human mathematics. Any interesting verified result would, obviously, be rewritten back into natural language for human understanding and consumption (as well as potentially for the benefit of AI conjecturers too). You are falsely assuming that advances in formal mathematics would not feed back into similar (potentially massive) advances into informal mathematics, and I think that's simply wrong. We're just at the very, very beginning of that curve.

I think this is, in fact, inevitable. It's the exact same RL loop that allowed AlphaGo to vastly exceed the world's top human players. You can theoretically RL formal proof techniques vastly beyond human capability by removing the need for any human review for correctness. It is completely reasonable to assume that "informalization" will become a real sub-field of mathematics in the near future.

Post reply on HN