In a way, this task is perfectly suited for LLMs. To even understand the problem statement, much less the proof or Lean, is an extremely specialized skill. The overwhelming majority of people who are aware of this news simply don't have the capacity to call BS. Maybe there are a few thousand people in the world who could, and it seems they haven't yet, but indeed it's only been a few weeks.

The more familiar analogy was when I look at the code that Claude spews for my partner. They take it at face value and hope it works. I usually find it very problematic, but only because I knew what to look for.