There has already been a formally verified proof of the Collatz Conjecture. The AI agent formally verified it by exploiting previously undiscovered bugs in Lean

There has already been a formally verified proof of the Collatz Conjecture. The AI agent formally verified it by exploiting previously undiscovered bugs in Lean. The Collatz Conjecture is still unsolved. > Let's say tomorrow someone comes up with a formally verified proof that a major encryption algorithm underpinning the security of the internet can be trivially broken, but they can't explain it. You're saying it should be kept under wraps and not published? Absolutely. It could also be exploiting bugs in the verifier. Even if not -- even if that proof were correct and entirely written by humans, care should still be taken in how such knowledge is published. I'd want to give trusted parties a chance to try to fix the issue before letting it be known by black-hats, for instance.