"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".

The data stealing company seemse to be stealing data

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.

Ja. Wenn die KI bei der Forschung hilft und die Firma/KI so an die unveröffentlichten Ideen kommt, ist es klar, dass die Firma dann absichtlich oder aus Versehen auf die Idee kommt, das selbe zu erforschen.

Edit: either my memory is betraying me, or there was a German article linked here before.