"Hey, I proved the Collatz Conjecture!", proompter says one day before severe bugs disclosed in theorem provers

⚠️⚠️[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.