Human Web CollectiveLLM mathematical proof exploits theorem proover bugs
infosec.exchange/@0xabad1dea/117002106099986943
Okay, we have a new contender for Most AI Thing to Ever Happen
1) July 25th: someone messes around with an LLM and posts a proof of the Collatz conjecture that does, in fact, verify in the theorem prover. (The AI use is not disclosed on the github page) https://
github.com/xrchz/CollatzLean
2) July 26th: several serious bugs are posted in the theorem provers, that in principle could allow a false statement to be “proven” true. They’re serious, yes, but no need for panic, because you’re not going to blunder into accidentally exploiting the bugs while writing a proof, probably.
https://
github.com/leanprover/lean-kernel-arena/pull/81
3) July 28th: someone who was right to be very skeptical of the Collatz proof, and had the expertise to study it with a fine-toothed comb, discovered it was exploiting a bug https://
github.com/leanprover/lean4/issues/14576
4) The “proof” turns out to be exploiting multiple similar but distinct bugs to pass different solver variants!
5) the human who posted the proof acknowledges the AI use and claims they did not knowingly point it towards the bugs it exploited. https://
leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Counterexample.20to.20the.20Lean.20Conjecture.20.28Soundness.20Bug.29/near/613135216
Note that the proof was posted shortly before the related bug reports were posted. It is an open question if the AI found people discussing the bugs shortly before they were formally posted and “decided” to exploit them, if the AI “knew about it” as a learned strategy from the training stage (putting every single “proof” it’s ever made and ever will make into profound doubt), or if it’s recently been repeatedly blundering into it by sheer stupidity and that’s how people noticed the bug at about the same time.
Theorem provers aren’t magic, and have bugs just like all other programs. They are tools to help us double-check our reasoning. When you skip the reasoning and ask an AI to “prove” something for you that’s over your head, you’re entering an adversarial pact with the monkey-pawed Devil of Customer Satisfaction.
4 Comments
Comments from other communities
fullsquare⚠️⚠️[IMPORTANT EDIT: it was later clarified that the person who originally posted the proof was already aware that it was buggy, and chose not to be clear about this up front, as a humorous way to file a bug. It’s pretty clear from the discussion threads that plenty of qualified people did not immediately realize it was meant to be a bug report.]⚠️⚠️
Well done on the use of the monkey paw.
Freaking wild… 😭
Extremely funny. There’s a similar situation in math where almost everybody is implicitly using one set of axioms (ZF/ZFC) because they’re highly expressive, intuitive, and not known to be inconsistent. There’s a hypothetical scenario where somebody discovers a proof that ZF(C) is inconsistent, rendering the vast majority of mathematics “invalid.” But nobody is really concerned because on a purely intuitive level, you should be able to transfer the vast majority of mathematics to a different formal basis without issue, since it’s all generally done at a different level of abstraction anyway. You’d have to somehow accidentally exploit the inconsistency of ZF(C) to get bit, which is unthinkable. … Unless you’re an LLM, I guess.
Next step we just need an LLM social engineer lean maintainer and introduce a bug they can then exploit.