that's not the claim. the formal statement of the problem for the NS proof was written by humans not autoformalized.
https://github.com/google-deepmind/formal-conjectures/blob/8...
Maybe read the comment before replying, at a minimum.
i havent seen this sentiment expressed anywhere, have you?
isn't this comment chain on a submission about openai's claims being reviewed?
The proof was released in the spirit of being first at all costs without any attempt to clean it up. I doubt that OpenAI mathematicians could give a coherent talk about it, certainly not using a blackboard.
A good review does not merely check the correctness of logical arguments, it gives suggestions for the exposition, citing the correct references, putting everything in the right context, etc.
Prestige to the reviewed, not to the reviewer.
Good, I just wanted to point out that peer review isn't primarily an arbitrage of truth, it is also to make sure the exposition is nice to read. When you get a reviewer who actually cares, you receive lots of feedback that isn't related to the correctness of Lemma 3.14.15 and stuff like that.
No. The way to build confidence that your software is well made, you do a proper external security audit and obtain the requisite certificate from a proper auditing firm.
It's also incorrect to think peer review in mathematics is low quality (like it is in some other fields). Certainly, when major results are in place, editors ensure that high quality peer reviewers are recruited and do their job properly. Like all human processes this fails sometimes, but not enough to not do it.
which specific openai statements does this part of your analogy map to?
in the "sharing ai progress in mathematics" blog, openai simply says "results", and never once claims that all of them are unquestionably true. instead, they state they want to evaluate the results. their github states that the results are "different stages of verification" and also says "Some of the unformalized results could have issues"
that is the opposite of "claiming [...] their software is secure", to use your analogy.
are people not reviewing openai claims right now?
openai themselves specifically call out that there may be issues with their results. journalists and laypeople just happen to skip that part, like they do with ~all physics, health, astronomy, etc results.
Peer review is a proxy for correctness.
Peer review journal is a proxy for quality peer review, or at least it was, once upon a time.
This is far more efficient and they’re telling the academic industry to grow up
Sister comments are saying that academics dont like the Lean programming language and see a lack of human language described proof. Doesn’t sound like something I should care about but I’m watching for a better human language description of the problem as this discussion evolves
yet i have never seen anyone say "the idea that physicists are beyond peer review is harmful" because some mainstream news articles published a piece about dark energy or whatever.