Comment by strangescript

This is a step beyond baseless predictions. Tao also had a "weird" "hypothetical" comment about LLMs solving complex proofs with impossible to human verify Lean.