Glossary
Formal proof
A mathematical proof written in a precise computer language so that software can check every step.
A formal proof is a proof written in a strict language that a program called a proof assistant can check mechanically. Lean is one widely used proof assistant; others include Coq (now Rocq) and Isabelle. If the checker accepts the proof, every logical step follows from the stated assumptions.
Formal proofs matter in AI news because they offer a way to verify an AI system's mathematical claims without relying on human reviewers to catch subtle errors.
A formal check confirms only that the proof matches the statement as written in the formal language. If the statement was translated from ordinary mathematics incorrectly, the proof may not establish what was claimed. Informal proofs written in normal mathematical language still need expert review.
Read more: our explainer