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