We appreciate comments from Christopher Henson, Zeke Medley, Ankit Kumar, and Pete Manolios. This post was initialized by Max's twitter thread.

Introduction

There's been a lot of chatter recently on HN and elsewhere about how formal verification is the obvious use-case for AI. While we broadly agree, we think much of the discourse is kinda wrong because it incorrectly presumes formal = slopless.[1]Over the years, we have written our fair share of good and bad formal code. In this post, we hope to convince you that formal code can be sloppy, and that this has serious implications for anyone who hopes to bootstrap superintelligence by using formality to reinforce “good” reasoning.

A mainstay on the Lean Zulip named Gas Station Manager has written that hallucination-free program synthesis[2]is achievable by vibing software directly in Lean, with the caveat that the agent also needs to prove the software correct. The AI safety case is basically: wouldn’t it be great if a cheap (i.e. O(laptop)) signal could protect you from sycophantic hubris and other classes of mistake, without you having to manually audit all outputs?

A fable right outta aesop

Recently a computer scientist (who we will spare from naming) was [...]

---

Outline:

(00:23) en-US-AvaMultilingualNeural__ Detective-style conspiracy board showing various programming vulnerabilities and code exploits connected by red strings.

(00:37) Introduction

(01:37) A fable right outta aesop

(03:02) Your formal model might not be proof-idiomatic.

(04:42) Mind the (semantic) gap

(05:48) A formal proof might not prove the thing you think it proves.

(09:04) Interactive theorem proving is not adversarially robust

(09:10) Axioms

(10:19) Backdoors

(12:22) Proofs of false

(13:12) Conclusion

(13:41) What are the bottlenecks?

The original text contained 9 footnotes which were omitted from this narration.

---

First published:
January 12th, 2026

Source:
https://www.lesswrong.com/posts/rhAPh3YzhPoBNpgHg/lies-damned-lies-and-proofs-formal-methods-are-not-slopless

---

Narrated by TYPE III AUDIO.

---

Images from the article:

Detective-style conspiracy board showing various programming vulnerabilities and code exploits connected by red strings.

Apple Podcasts and Spotify do not show images in the episode description. Try Pocket Casts, or another podcast app.

“Lies, Damned Lies, and Proofs: Formal Methods are not Slopless” by Quinn, Max von Hippel

LessWrong (30+ Karma)

“Lies, Damned Lies, and Proofs: Formal Methods are not Slopless” by Quinn, Max von Hippel