41–50 of 467 posts
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. 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…
I suspect the value is in showing the potential that LLMs have in developing new breakthroughs.
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.
Announcement: https://x.com/__eknight__/status/2075643450196971805 Prompt: https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98...
I wonder what the survivorship bias is though. How many other problems did they try but fail? Did they try to solve this problem but with another prompt? Still very impressive though.
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.
Throughput Output tokens Output cost
---------------------------- ------------- -----------
40 tok/s (5.5 low) ~9.2M ~$275
55 tok/s (5.5 base) ~12.7M ~$380
70 tok/s (5.5 high) ~16.1M ~$485
750 tok/s (Sol Fast, $75/M) ~172.8M ~$13,000
Edit: better tok/s estimate buckets based on GPT 5.5 actual speeds since I couldn't find real benchmarks on 5.6 published anywhere. Also account for Sol Fast pricing.
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…
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)
What is the perfect video game that makes the user infinitely happy?
What is the perfect economy optimizing program?
What algorithm can solve political strife?
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…
Its the same with proofs. First time someone proves something gets a lot of credit. The second proof for the same theorem gets a lot less buzz.
But even then, math proofs mostly get buzz when its something famous or at least important. Proving a random lemma usually doesn't get much buzz.
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…
Yes, the math department.
In any case linear algebra, stochastics, calculus; plenty of engineering and science applications for all these.
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. 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…
No, the value is that Erdos's name is attached to it.
Lots of mathematicians prove things they don't publish, or their manuscripts get rejected - not because of a flaw in the proof but because no one cares about the theorem they proved.
And I'm sure it'll be the case with LLM models performing proofs. It'll be notable only when the theorem is a known one that people have had difficulty proving.