Birbla

Join the discussion

Write your take first — we'll ask for email only when you're ready to publish.

Sign in
  • Hacker News
  • What a timeline, OpenAI's model is so good, it publishes hundreds of math papers.

    The latest model even finds mistakes in previously published math papers!!!*

    * so far, only OpenAI's math papers were faulty and needed retraction.

    by nairboon
  • 3 mistakes (so far) out of ~400 is still a pretty good hit rate
    by hmate9
  • It seems one of the errors was a sign error. If sign errors have high probability then there is high probability of having other false proofs, moreover sign error are similar to error in basic operations, so there could be many basic type errors. So I think our prior about false proofs is now a posterior with a higher probability for false proofs.

    Edited.Added. To compute the posterior one needs to know the probability of detecting such error in a proposed proof.

    by Trusteando
  • If you do a dump like this all of it should be formalized, there's simply too much material to review by hand and additionally it is AI-written which makes it hard to read compared to human work.
    by margorczynski
  • I find the paper about beating O(n log n) for integer multiplication also quite fishy, not sure but it seems like too good to be true, I feel like there must be a subtle flaw in that. Maybe that's just me hating these small numbers in the paper, but it seems wrong, unnatural even! I would be similarly skeptical about a physics paper that claims to be able to exceed the speed of light by a tiny fraction. There's no reason n log n is the natural limit here but I see a few good intuitions so having something else that can't be represented in an elegant form seem very "unmathematical" to me.
    by ThePhysicist
  • This is what it looks like when software engineering practices meet mathematics. "openai/math release 1.3.42: retracted papers 139 and 140, fixed a sign error in paper 47, restored previously retracted paper 85, refactored the arguments in paper 101".

    I'm curious to know if the withdrawal was due to an actual mathematician looking at the papers and noticing the errors, or they ran a model on these to proofread, which would not be the first time, presumably, since they would have surely done that before publishing. Both options have interesting implications.

    by renyicircle
  • I think that on closer inspection, a lot of these fully AI generated proofs will fall apart. Even in Lean, you can build theories which compile but nonetheless state something different than what you actually intend. It's just that the volume of proof is so staggeringly large that it will probably take years before we find the issues, a la abc conjecture
    by ijustlovemath
  • So were the 3 withdrawn proofs the ones without Lean verification?

    If so, why did they mix proofs that were verified with Lean, and proofs in natural language?

    I was wondering that while reading Aaronson's blog:

    https://scottaaronson.blog/?p=10169

    Or at least, we’re pretty sure that it’s a proof! There’s a Lean certificate, as there are for some of the other 372 breakthrough results (not all of them). But it also appears that no human has understood just about any of these proofs yet

    It seems that the obvious thing to do would be to release in TWO parts: the ones that are verified, and the ones that might have some good ideas but also might have some mistakes. Presumably the latter would be much more epxensive for humans to verify.

    by chubot

Explore Birbla archives