The speaker says a formally checked proof may prove the wrong proposition, so a person must verify that an AI-generated Lean statement accurately represents the intended conjecture, definitions, and assumptions.

“But a checked proof can still be a proof of the wrong thing. When an AI produces a lean proof of a famous conjecture, someone must still establish that the formal statement captures the intended conjecture with appropriate definitions and assumptions.”