In short
In short: formal verification translates a claim - a mathematical proof or a program's behavior - into a language a machine can check line by line. Systems like Lean, Coq and Isabelle do not accept almost right: if one step is missing, the whole proof fails. Which is why a formally verified result does not depend on who wrote it - a person, a team or an AI model.
The difference from ordinary review is the difference between a taster and a scale. The taster is experienced but human: gets tired, misses things, sometimes wants the result to be true. The scale wants nothing. It shows what is.
That is exactly why formal verification matters in the model era. Text from a model can sound flawless and be wrong in the middle. Once it passes Lean, the question of who wrote it stops existing. A verified step is a verified step.
Do not trust the author. Do not trust the machine either. Trust the check that does not accept almost.
Where you meet it
In mathematics, when a result from an AI system seeks legitimacy. In critical software: avionics, medical devices, operating system kernels. And more and more in the AI safety conversation - as the only kind of answer that does not depend on the honesty of whoever is answering.
Primary sources
Lean: the prover's official siteThe visual is generated code-art, no third-party images.