✳flâneur — a map of the web's best reading

Broken proofs and broken provers

lawrencecpaulson.github.io · 1,587 words · saved by 1 readers

People expect perfection. Consider the reaction when someone who has been vaccinated against a particular disease nevertheless dies of it. Mathematical proof carries the aura of perfection, but again people’s expectations will sometimes be dashed. As outlined in an earlier post, the verification of a real world system is never finished. We can seldom capture 100% of reality, so failure remains possible. Even in a purely mathematical proof, there are plenty of ways to screw up. Plus, proof assistants have bugs. Many years ago, I refereed a paper about the verification of some obscure application. I recall that the theoretical framework depended on several parameters, among them z 𝑧 , a nonzero complex number. This context was repeated for all the theorems in the paper: each included the assumption ∀z.z≠0 ∀ 𝑧 . 𝑧 ≠ 0 . Needless to say, that assumption is flatly false. The author of the paper had presumably intended to write something like ∀z.z≠0→⋯ ∀ 𝑧 . 𝑧 ≠ 0 → ⋯ . The error is e

Broken proofs and broken provers Machine Logic At the junction of computation, logic and mathematics Broken proofs and broken provers 15 Jan 2026 [ general verification Isabelle memories ] People expect perfection. Consider the reaction when someone who has been vaccinated against a particular disease nevertheless dies of it. Mathematical proof carries the aura of perfection, but again people’s expectations will sometimes be dashed. As outlined in an earlier post , the verification of a real world system is never finished. We can seldom capture 100% of reality, so failure remains possible. Eve

Explore this link on the map →

related reading