“An apparently AI-generated formal proof, in Lean, purporting to be a disproof to the…”
Machine Learning Street Talk @MLStreetTalkX
Archived text
An apparently AI-generated formal proof, in Lean, purporting to be a disproof to the Collatz conjecture, was actually exploiting a bug in the Lean kernel!
EXCLUSIVE from Lean Creator Leo de Moura:
“This is going to keep happening. AIs are really good at exploiting soundness bugs in the kernels.”
It appeared to pass both Lean’s official kernel and Nanoda by hitting two separate bugs.
Both have now been patched - @Leonard41111588.