Comment by j2kun
7 hours ago
I think this highlights that, at the very least, coverage of AI-generated proofs should describe them as "claims" to solve problems, until, like all other works, the community has had time to review and digest them.
The idea that an AI company is beyond peer review is harmful.
As far as I understand it, nobody is disputing the correctness of the Lean proof, or that it proves the conjecture it actually claims to prove. That's sufficient to consider the problem "solved". The natural language proof is a "nice to have".
The claim in TFA is that the formalization(in Lean) of the problem does not correspond to the natural language statement of the problem, such that the statement proven is not the conjecture for which proof is required for the problem to be considered "solved".
>the statement proven is not the conjecture for which proof is required for the problem to be considered "solved".
that's not the claim. the formal statement of the problem for the NS proof was written by humans not autoformalized.
That's not the claim made in TFA. See the sibling comments, in particular about the DeepMind formalization.
[flagged]
Please make your substantive points without swipes. This is in the site guidelines: https://news.ycombinator.com/newsguidelines.html.
Does that contradict what I said? In that quote, it says that the NL proof does not correspond to the Lean proof. However, the statement of the theorem in Lean is independent from the NL proof. It comes from a DeepMind repository, which as far as I'm aware has been accepted by the community as a valid formalization of the original Clay Institute statement.
https://github.com/google-deepmind/formal-conjectures/blob/8...
1 reply →
Both proofs may be correct, and the problem may indeed be solved. My point is that it should not be assumed.
> Maybe read the original article before replying, at a minimum.
Maybe read the comment before replying, at a minimum.
>The idea that an AI company is beyond peer review is harmful.
i havent seen this sentiment expressed anywhere, have you?
isn't this comment chain on a submission about openai's claims being reviewed?
OpenAI has expressed this sentiment by not submitting to or saying they will submit their results to peer reviewed journals.
I would say it's released in the spirit of open source. "Peer review" in the narrow sense exists primarily to assign prestige in academia; but there's nothing stopping anyone from "peer reviewing" the GitHub repository.
12 replies →
not submitting to whatever journal is quite different than saying they are "beyond peer review"
are people not reviewing openai claims right now?
2 replies →
You are confusing two levels of indirection here.
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.
Because they want to release everything on github so everyone can peer review it themselves
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
"not interested in" != "beyond"
I've seen a lot of breathless reporting about various mathematical things being "proven" on the basis of the LLM-generated Lean formulation compiling. We probably wouldn't declare that for a human-written proof until peers had checked the proof for errors
This. The proof of Fermat’s Last Theorem took 15+ months to check. It’s absurd to see the media reporting that these big problems are solved based off of a news release and a hastily and mostly AI-written manuscript, and OpenAI et al. are all too happy to run with said breathless reporting.
1 reply →
there's breathless reporting of just about everything scientific. physics, astronomy, archaeology, etc. have this sort of thing all the time.
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.
Exactly. Coverage here is "OpenAI has solved problem X", not "OpenAI has claimed to solve problem X."
Anyone who doesn't understand peer review (its intended workings, its negative effects by implementation flaws, etc.) automatically assumes expression is beyond academic peer review, so thats potentially a lot of people...