← Back to context

Comment by viraptor

6 hours ago

Have you got a link to someone pointing it out? It looks like they're still going through formal proofs so likely found the problems that way.

21 comments

viraptor

Reply
sanxiyn  5 hours ago

Yes: https://x.com/ElliotGlazer/status/2108026240582246600

  • viraptor  5 hours ago

    So someone ran a different LLM to find an issue they'd find anyway during formalisation? That's not the same as relying on thriving community.

    • oliculipolicula  5 hours ago

      The bigger question is why there was internal pressure to rush such a historic launch without having someone in the company, anyone, check the proofs first.

      This concerns the Hodge conjecture (millennium prize related) paper. Seems to me like PhD nerds weren't confident bosses pushed ahead anyway.

      11 replies →

    • verdverm  3 hours ago

      I would say

      1. This is expected if you only use a single model family like Claude, eg. we use a different model family for code review than authoring, OAI could have done this too for their math dump

      2. Ai needs a good human driver beyond the trivial or mundane, they are expert enhancing machines, not expert creating machines. This is where the community comes in. Reading Tao's ChatGPT session reveals this: https://news.ycombinator.com/item?id=49010345

      3. OAI is not trying to be a member of the/any community, this is not the first story to shows this, nor do I expect it to be the last. Perhaps this is them being effective altruists today? /s

  • afavour  5 hours ago

    That’s not proof though is it? If the original LLM output is fallible surely the LLM review of that output is also very much fallible?

    • rsfern  5 hours ago

      Proof of what? There is a sign error in one of the proofs, OpenAI acknowledged it and withdrew three papers (two relied on the result).

      I agree LLM review is also fallible (as is human review) but the interesting part to me is that finding this sign error before publication should have been table stakes for OpenAI, it’s their own model that found the sign error.

      I’m curious what was in the original prompt and what was in the prompt that led to finding the sign error, I think it matters a lot for understanding the dynamics here

    • kolinko  4 hours ago

      Output of LLM can be infallible* even if LLMs themselves make mistakes. Ditto with humans.

      As much as anything can be infallible.