← Back to context Comment by Xenoamorphous 4 days ago Including those with Lean verifications? 2 comments Xenoamorphous Reply anonymous_user9 4 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.
anonymous_user9 4 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.
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.
Yes, for all we know they're exploiting a bug in Lean.
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.