Formal Verification Has a Trust Problem Now

A soundness bug in the Lean proof kernel (issue #14576) allowed a 'sorry-free' disproof of Collatz to pass the verifier. The postmortem thread was blunt: if an LLM can produce code that fools the formal verifier itself, the guarantee that made formal proofs attractive collapses. The comment that landed hardest was simple: 'One cannot trust the code produced by an LLM, even if the code is a formal proof passing the verifier.'

This lands directly on top of OpenAI's claim that its internal Astra model solved 10 major open math and CS problems. The HN thread on that was deeply skeptical, with commenters noting that the marketing loop around AI math breakthroughs is so well-worn it's become a meme. The pattern: a result is announced, the community can't verify it independently, and the hype cycle runs anyway.

The counterpoint some raised is that the Lean bug was found and fixed quickly, which is exactly what open, auditable systems are supposed to do. But the damage to the narrative is real: the appeal of using LLMs plus formal proofs as a trust layer for AI-generated code just got harder to sell.