formal-verification

Proof assistants: why a machine-checked proof beats a convincing one Lesson

A proof assistant is software like Lean or Coq that checks a mathematical proof step by step against strict logical rules, so a proof is accepted only if the machine confirms every inference -- which is exactly why the field demands them when an AI claims to have proved a theorem.