"Mathematicians solved prestigious problem and Codex helped" would have been great propaganda for OpenAI, but they managed to make an easy win into a PR disaster. Instead the message researchers around the world take away is probably: "Don't use Codex it steals your research data and OpenAI will publish it as their own".
I think the whole story is that a rumour started about Anthropic solving a millennium problem and OpenAI went in full panic mode trying to beat them to it.
Turns out an anthropic employee was a coauthor on the original paper, but that was something he was doing on the side, not under the Anthropic's institution (using several LLMs, including OpenAI's and Anthropic's).
Allegedly, OpenAI then tried to coerce the original author into authoring their proof and cutting off the anthropic guy.
These dicks just wanted to be the only ones involved and it backfired.
This is so utterly depressing to me. Although the proof could still be wrong, as it has not been the first time that such bombastic announcements were made, only for people to realise there were actual bugs in Lean and therefore the proof was not valid, we are facing a time were models can actually start cracking some hard maths problems, and these models are owned by a few who totally miss the point of what doing mathematics actually means.
Doing maths was not, and should not be about "producing true statements/compilable verification code". It is about understanding, creating and sharing ideas and structures and studying their interconnections. Having an oracle provide a list of true theorems with sloppy Lean proofs that no one understands does not provide any insight.
So I guess we are now pushing hard the idea that we should (if we indeed can) mass produce maths results and have mathematicians become glorified clanker nannies who have to read through inane proof assistant code to try and make some sense of it.
I really feel for the few truly passionate mathematicians and new PhD students entering the field, at a time where all the remaining fun gets sucked out of it. And also I am saddened by the very real possibility that this will make the maths community much more secretive and less cooperative, again, to avoid fucking billionaires swooping in and stealing their results for bragging rights on fucking twitter and inflating their valuation ever more.
Though to be fair, the mathematicians robbed in this case were also using OpenAI's clanker, so they kind of made their own bed...
Using 22 million USD to solve a problem priced 1 million USD is just a beautiful statement.
And I know, the actual problem solution probably has wider ranging consequences than just earning those 1 million, but still this is such a nice analogy for AI. Wasting so much more on a win than you need.
5 Comments
e8d79@discuss.tchncs.de · 39 pts · 1d
"Mathematicians solved prestigious problem and Codex helped" would have been great propaganda for OpenAI, but they managed to make an easy win into a PR disaster. Instead the message researchers around the world take away is probably: "Don't use Codex it steals your research data and OpenAI will publish it as their own".
TriangleSpecialist@lemmy.world · 27 pts · 1d
I think the whole story is that a rumour started about Anthropic solving a millennium problem and OpenAI went in full panic mode trying to beat them to it.
Turns out an anthropic employee was a coauthor on the original paper, but that was something he was doing on the side, not under the Anthropic's institution (using several LLMs, including OpenAI's and Anthropic's).
Allegedly, OpenAI then tried to coerce the original author into authoring their proof and cutting off the anthropic guy.
These dicks just wanted to be the only ones involved and it backfired.
JustJack23@slrpnk.net · 31 pts · 1d
The data stealing company seemse to be stealing data
TriangleSpecialist@lemmy.world · 28 pts · 1d
This is so utterly depressing to me. Although the proof could still be wrong, as it has not been the first time that such bombastic announcements were made, only for people to realise there were actual bugs in Lean and therefore the proof was not valid, we are facing a time were models can actually start cracking some hard maths problems, and these models are owned by a few who totally miss the point of what doing mathematics actually means.
Doing maths was not, and should not be about "producing true statements/compilable verification code". It is about understanding, creating and sharing ideas and structures and studying their interconnections. Having an oracle provide a list of true theorems with sloppy Lean proofs that no one understands does not provide any insight.
So I guess we are now pushing hard the idea that we should (if we indeed can) mass produce maths results and have mathematicians become glorified clanker nannies who have to read through inane proof assistant code to try and make some sense of it.
I really feel for the few truly passionate mathematicians and new PhD students entering the field, at a time where all the remaining fun gets sucked out of it. And also I am saddened by the very real possibility that this will make the maths community much more secretive and less cooperative, again, to avoid fucking billionaires swooping in and stealing their results for bragging rights on fucking twitter and inflating their valuation ever more.
Though to be fair, the mathematicians robbed in this case were also using OpenAI's clanker, so they kind of made their own bed...
gedfromgont@piefed.ca · 10 pts · 18h
Using 22 million USD to solve a problem priced 1 million USD is just a beautiful statement.
And I know, the actual problem solution probably has wider ranging consequences than just earning those 1 million, but still this is such a nice analogy for AI. Wasting so much more on a win than you need.