@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.
An extremely lightweight universal grammar implementation with provable recursion, based on Chomsky's Minimalist Grammar theory, fitting in under 50kB with zero runtime dependencies. It includes a probabilistic language model extension and formal verification.
