I'm having a really hard time seeing how this letter could conceivably be perceived as persuasive. In fact, this letter makes it clear that the people behind it are seeking to maintain their previously entrenched power, prestige, and control over a field of human knowledge. And they are going about it in a futile and debasing way.
As I understand it, this is one of the groups OpenAI claimed to be consulting with to improve their process after the Navier Stokes fumble. I think OpenAI might have even said something like “in accordance with this group’s guidance” in the big dump? So this post should be read as distancing themselves from OpenAI and denying any legitimacy OpenAI tried to derive from their association.
Edit: on researching more, I don’t think this is the case; I must have confused them with some other group.
they could have definitely written it better and put more effort into it. As it is, they have real gripes with how openai is doing things and i think they should have concretely listed their objections. Either way, if OpenAI dumps a gazillion proofs, who actually is going to read them, understand them, assess their correctness etc... ? If no one is doing that, is that problem really "solved" ? So OpenAI just dumps proofs and calls it a day, or this trillion dollar company can spend some effort engaging with mathematicians but really OpenAI doesn't really care about Math, they want to prove that their frontier intelligence can just do it all before they IPO. You say the authors are trying to maintain their power, but what is OpenAI doing? Certainly, you are naive if you think they are doing this stuff for the benefit of humanity or a goal of advancing mathematical knowledge.
Who knows, If compute keeps dumping proofs for problems but no one knows their correctness because mathematicians stop investing their time in understanding these proofs, then you can't even really use the results.
Imagine a world in which problems are mined, proofs are generated, yet no one exists to understand or verify the correctness of these proofs. In software parlance, who is going to review all the vibe coded bs that come your way if you maintain an open source library - is the open source maintainer standing in the way of 'progress'? Really, this whole scheme only works if AI were truly autonomous beings, i.e they have a system where they can verify their proofs, use it to understand which problems they need to tackle next, build understanding which is used by other AI to generate tools to solve physics problems etc... but the way we are approaching things does not work if humans are heavily in the loop.
Isn't the big problem here that volunter work is being exploited by billion dollar companies? Of course it's bad and there should be a solution where openai pays people to verify the information they put out in the public before it ever reaches independent reviewers.
Of course the dinosaurs chose to bury their heads in the sand, and asked that everyone else does too. They've no place in the new world. They could've instead come up with good feedback to improve the paper quality, but they didn't.
„Mathematicians did not ask for this work to be done.”
Since when science works like this?
One point I might slightly agree with - refusal to acknowledge work done with nonpublic models. Otoh in other fields and in history it’s been common to do science with resources unavailable to common people.
Nobody needs permission to solve an open problem. That's the whole point of publishing them. The question for any result is whether it's correct, not who produced it or whether anyone requested it.
Bringing up OpenAI's lawsuits is irrelevant to whether these proofs hold. And calling a release that includes Lean formalizations a "demonstration of power" gets it backwards. Machine checkable proofs are the least "trust me" form of mathematics there is.
There are fair criticisms here. Not every result is formalized, the model can't be reproduced by outsiders, and the massive dump strains review capacity. Those are reasons to demand full formalization, open access to the methods, and help funding human review. They aren't reasons to dismiss correct mathematics or to tell people to stop working on hard problems.
A depressing statement that does nothing to increase people's support of working Mathematicians. It feels like a low-effort political hit as opposed to the balanced writeups we've been reading from top Mathematicians like Terence Tao.
Edit: on researching more, I don’t think this is the case; I must have confused them with some other group.
Certainly you are cynical if you think it won't benefit humanity or advance mathematical knowledge.
Gatekeeping much?
"Mathematicians have a particular vision of progress that is informed by history and field-specific considerations."
This cannot seriously have been written by anyone mathematically literate, it's just too embarrassing.
It's just sour grapes.
Related:
“Math 2.0” will need to value mathematical progress more holistically
https://news.ycombinator.com/item?id=50002008
Since when science works like this?
One point I might slightly agree with - refusal to acknowledge work done with nonpublic models. Otoh in other fields and in history it’s been common to do science with resources unavailable to common people.
Bringing up OpenAI's lawsuits is irrelevant to whether these proofs hold. And calling a release that includes Lean formalizations a "demonstration of power" gets it backwards. Machine checkable proofs are the least "trust me" form of mathematics there is.
There are fair criticisms here. Not every result is formalized, the model can't be reproduced by outsiders, and the massive dump strains review capacity. Those are reasons to demand full formalization, open access to the methods, and help funding human review. They aren't reasons to dismiss correct mathematics or to tell people to stop working on hard problems.
with no teeth, stuff like this starts to feel a little funny+sad