@0xabad1dea@infosec.exchange writes about an incident where AI-assisted mathematical proofs appear to exploit bugs in theorem provers, specifically highlighting a case involving the Collatz conjecture and Lean 4. The discussion explores whether large language models are inadvertently discovering software vulnerabilities through pattern matching or learning from existing technical discussions about those bugs, while broader debates address the inherent limitations of formal verification when facing hardware faults, modeling errors, and human mistakes in specifications.
