Flutterby™! : leanprover bugs and adversarial relationships with tools

abadidea @0xabad1dea@infosec.exchange posts about the AI generated (but not disclosed on the github page) proof of the Collatz conjecture that validate in the leanprover theorem prover, posted in July 25th.

Discussion of bugs leanprover on July 26th, on July 28 that proof exploited a similar bug, leading to acknowledgemnt of LLM use and discussion of the bug.

Additional discussion.

The rest of the thread talks about tools that assume good faith, like compilers, and how we're adapting to building tools that assume adversarial relationships with the users of them.