Hacker News Reader

It sounds like OpenAI is trying to appease the author when they don’t have to by allowing him to rewrite their proof. They probably don’t believe he deserves to, so him asking for a coauthor from Anthropic might overextend their grace in their eyes.

View on HN

He's not "asking for a coauthor from Anthropic"; he already has a coauthor, who he's already been collaborating with, who happens to also be employed by Anthropic (but whose research in this area is not done as part of their employment at Anthropic).

Given that Tristan has said that the proofs that LLMs come up with are mostly "slop" and not up to the standard that human written papers achieve, maybe OpenAI needs an expert like him more than you think to get the result published?

Almost certainly the Lean proof needs to be decoded for humans and probably also made “human intelligible”.

Now maybe LLMs can also simplify arguments and make sense of them for humans, but we haven’t seen that yet (unaided).

(I haven’t looked at it, personally.)

It's a Navier Stokes solution.

They don't need any help publishing.

Reply on news.ycombinator.com