Post #4193509

2026-07-29 10:24 UTC

A little bit of plot thickening spotted by abadidea: infosec.exchange/@0xabad1dea/117002106099986943 tl;dr, the timeline looks like this: “proof” of collatz conjecture released bugs identified in lean kernel proof demonstrated to use these bugs There was only a day between the first two events, and the non-proof was not where the bugs were discovered. So maybe it was just a coincidence that the chatbot found the bug at the same time, or maybe it’s training data included previous investigations into those bugs which it then built upon and that would be a bad thing for other llm generated proofs. The collatz conjecture is sufficiently famous that enough third-party checking was done to sort the problem. I wonder how much checking would have been done on proofs of less famous and interesting things.

Replies (1)

@rook@awful.systems 2026-07-30 09:20

And a follow-up by talia ringer, who observes that there have always been gaps between the type-theoretic underpinnings of things like the lean prover and their actual implementation, and this hasn’t been so much of an issue til now because theorem provers haven’t had the attention of people in high places, and the type-theoreticians have been able to catch up in due course. mathstodon.xyz/@TaliaRinger/117005740997367321 My big worry right now is that if organizations continue to fund the crap out of Al for formal proof research (and to generally support implementation and maintenance of proof assistants like Lean as part of that effort) but don’t bother funding the type theory side of things, those gaps will grow larger and will be exploited more often by Al tools via reward hacking. Whereas people tend to only exploit kernel bugs to make a point that the bug exists. Thus proof assistants will grow less trustworthy over time. Anyone want to place any bets on whether or nor the big llm companies are going to fund academic research that isn’t obviously mechanisable right now and won’t yield any clickbait headlines?

Open ##4235205