Hacker News new | past | comments | ask | show | jobs | submit
zahlman | on: Ten advances in mathematics and theoretical computer science
Indeed. It seems to me much more likely that the AI was directed to look for bugs in Lean, found one, and then it was directed to write a proof specifically targeting the bug.