← Back to context

Comment by gus_massa

2 days ago

Too late to edit:

"10 or 20" -> "10 or 20 years"

Wow!

If curl developers are overwhelmed by AI PRs, imagine how mathematicians will feel verifying a huge backlog of automated proofs.

Or isn't there such a thing? Can someone make a very complicated automated proof that ultimately reveals itself to be useless?

  • For math it's easy, everyone just ignore it. There is no Daniel to blame. There are a few post about P=/!=NP or the Riemann conjeture or rewriting physics each week that are posted to HN. I'm just ignoring them. Other mathematicians are just ignoring them. But you will not find anyone to blame.

    There are a few "solutions" of conjetures that may be correct, like https://news.ycombinator.com/item?id=45273999 in particular the first comment. Is that an heroic result that opens a lot of paths or a useless combination of tricks that no one will ever understand? (In my opinion a proof is a proof [standing applause emoji].)

    • What I (personally) consider insightful is irrelevant. It's about what mathematicians consider insightful.

      Mathematicians are obviously not ignoring automated proofs. Terry's post is an evidence of that.

      Consider LK99 instead of crackpot P vs NP proofs. That wasted a lot of academia time.

      It seems that it could happen to math.