Comment by anonymous_user9 3 days ago Yes, for all we know they're exploiting a bug in Lean. 1 comment anonymous_user9 Reply 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.
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.
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.