Formal verification turns an argument into a form a computer can check completely. In mathematics, a proof is written in a proof language such as Lean, and the checker either accepts every step or rejects the proof. In software, the same idea proves that a program meets its specification for every possible input, not only the cases someone tested.
It has become central to AI because machines now produce proofs and code faster than people can review them. A formal checker scales where human reviewers do not. That is why many mathematicians see it as the answer to an incoming flood of AI-generated proofs.
It answers one question only: does this follow from what we stated? It cannot say whether the statement was the right one to ask, or whether anyone understands why the result is true. Terence Tao’s question at the 2026 International Congress of Mathematicians, whether we could have a verified proof of a major result that no human understands, is about exactly that gap.