Lean

Lean is a proof assistant. You write a mathematical argument in it, and the software verifies every step against the rules of logic. If it compiles, the proof is correct, with no reviewer needed to take anything on trust. Mathematicians have used it for years to formalise big theorems.

It has become important in AI for one specific reason. When a model claims to have proved something, a Lean certificate turns that claim from a matter of opinion into a matter of fact, which is why AI labs now publish proofs in Lean alongside the prose version.