A proof checker can verify a derivation without ensuring that the formal statement correctly 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.”