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