22 points kkoncevicius 4 hours ago 13 comments
brap 1 hour ago | parent
Simulacra 1 hour ago | parent
asa123 57 minutes ago | parent
with no teeth, stuff like this starts to feel a little funny+sad
glimshe 51 minutes ago | parent
chank 39 minutes ago | parent
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.
kolinko 22 minutes ago | parent
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.
himata4113 16 minutes ago | parent
skwirl 15 minutes ago | parent
kccqzy 12 minutes ago | parent
sscarduzio 9 minutes ago | parent
fidotron 6 minutes ago | parent
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.