February 4, 2026
Proof or it didn’t compile
Broken Proofs and Broken Provers
When the math robots misfire, the internet asks: who checks the checkers
TLDR: A deep dive shows even proof-checking software can glitch—Isabelle once let a stuck proof slip due to multithreading. Commenters split between “trust but verify the verifiers,” skepticism about comparing bug counts, and war stories like a compiler flipping answers—raising real questions about certainty in our math machines.
Math is supposed to be perfect, right? Not so fast. A veteran dev reminded everyone that even “proof assistants” like Isabelle can slip, from papers torpedoed by a missing “if” to a wild multithreading bug that let a stuck proof sail through. The post even waded into the spicy “x/0=0” debate, arguing it only matters if you actually divide by zero. Cue the comments: systems folks swooned over the race condition drama—one called it the kind of subtle bug that means “verification tools need… verification tools.” Skeptics barged in with the stats fight, side-eyeing claims like “one soundness bug per decade” and warning that comparing bug counts across tools proves nothing.
Then came war stories. zero_k recalled a GCC hiccup that made a SAT solver swear a solvable problem was impossible. Translation: even your compilers can betray your math. Fans defended Isabelle’s safety nets (clear assumptions, warnings, batch-mode catch-alls), but memes flew anyway: “Sledgehammer fixes everything,” “x/0=0? Don’t look, don’t care,” and “Proof or it didn’t compile.” The core drama: Can we trust machines built for certainty when tiny, rare bugs lurk in every layer? The hive mind’s verdict: trust, but verify the verifiers—and never celebrate until batch mode signs off
Key Points
- •A global, incorrect assumption (∀z. z≠0) can invalidate an entire proof development; explicit premises help avoid this.
- •Isabelle’s Sledgehammer can warn about contradictions, and locales help manage shared assumptions across theorems.
- •A multithreading quirk in Isabelle can let proofs appear to succeed when a preceding proof is stuck; batch mode helps expose timeouts.
- •Incorrect definitions in proof assistants do not break consistency; they change theorem meanings but cannot force contradictions.
- •Isabelle, HOL, and Lean define behavior for division by zero; discrepancies only matter when division appears, and there is no traditional meaning for x/0.