TechnicalAI glossary
Formal verification
Rewriting a line of reasoning (a mathematical proof, a program) in a language where every step must be explicitly justified, then having it checked by software that mechanically verifies each deduction. If the checker accepts it, the proof is correct in the strict sense. It is gaining importance as AIs produce proofs too long for humans to read through in full.
In other words
A ticket inspector who knows nothing about the journey but checks every ticket, one by one: no one gets through without a valid one.
Alyriaz articles that mention it
- OpenAI releases 372 maths results at once
A secret OpenAI model produced 722 manuscripts, 372 families of results, posted online. How to check them, and why it divides.
- Is slowness a method?
Faced with results produced faster than they can be understood, we examine what slowness actually produced in knowledge, and what is lost when it disappears.
- The week of extraordinary claims
Week in review, 7–13 September 2026: Navier-Stokes, attribution disputes, Mistral, Suno v6, and data centres leaving the grid.
- Should we believe an extraordinary announcement?
When faced with a spectacular scientific claim, we examine what distinguishes methodical caution from performative scepticism, and which criteria allow us to form a judgement.
- The problems of the millennium, and how a proof comes to be accepted
Seven Millennium Problems were posed in 2000. We explain what they are, why only one has been solved, and above all how the mathematical community decides that a proof holds up.
- What is formal verification? Having a machine check a line of reasoning
Formal verification makes it possible to mechanically check every step of a line of reasoning. We explain the principle, its limits, and why it is becoming central as models produce proofs.