Slacker News Slacker News logo featuring a lazy sloth with a folded newspaper hat
  • top
  • new
  • show
  • ask
  • jobs
Library

Comment by Xenoamorphous

4 days ago

Including those with Lean verifications?

2 comments

Xenoamorphous

Reply

anonymous_user9  3 days ago

Yes, for all we know they're exploiting a bug in Lean.

  • gus_massa  3 days ago

    Sadly, if it were a bug the AI would have used it to prove everything, like in the human written hoax of the Collatz conjeture.

    Even if a person manually wrote a paper and 10 person manalluy reviewed it, it is possible that all 11 of them made a mistake.

Slacker News

Product

  • API Reference
  • Hacker News RSS
  • Source on GitHub

Community

  • Support Ukraine
  • Equal Justice Initiative
  • GiveWell Charities