← Back to context

Comment by margorczynski

3 hours ago

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.

13 comments

margorczynski

Reply
DonsDiscountGas  2 hours ago

Apparently the write-ups are garbage (as in very hard to read). I feel like they could've had AI fix that up at least somewhat. Maybe they'll reinvest more in writing ability now.

  • margorczynski  1 hour ago

    The write-ups are one thing and more of a cherry on top but I would say the more pressing matter is the lack of Lean formalization which means you can't really say it has been (dis)proven or not.

  • idiotsecant  2 hours ago

    I think the obscurity is a feature, not a bug. They don't want a headline where 250 of these results are invalidated overnight. They want rejections to trickle out and be buried.

andybak  2 hours ago

Not a mathematician but surely if a problem I was working on had an AI also working on it, I would want to know as early as possible - even with flaws or gaps. What advantage is it to me to be less informed?

  • baobabKoodaa  2 hours ago

    I can prompt ChatGPT right now and ask for mountains of more "mathematical work"; thousands and thousands of pages of nonsense for you to review. So you can "be informed".

    • andybak  21 minutes ago

      But you couldn't make me review it. Anyway I think you're just straw manning what I was trying to say. I probably didn't express it terribly clearly and I'm not invested enough in this debate to put any more time in.

    • cma  1 hour ago

      But you can't do it with their internal model that is the same or a successor to the one that solved the navier stokes millenium prize problem.

      With 40% formalized they probably have a good idea of how many were found to have fatal issues in the formalization attempt, and they hired some mathematicians to verify some of them, especially the big headline ones.

      1 reply →

  • ajs1998  1 hour ago

    Mathematicians are in no rush. And they are less likely to review math vomit that hasn't even been formalized and verified. Especially among the now thousands of vomit papers out there.