alt Hacker NewsKeep in mind the last big LLM maths proof (disproving the Collatz conjecture) turned out to just be exploiting five different bugs in LEAN
Keep in mind the last big LLM maths proof (disproving the Collatz conjecture) turned out to just be exploiting five different bugs in LEAN
That very much does not describe what happened. Someone found the bug and used it to disprove the Collatz conjecture as a demonstration of the bug. Nobody ever claimed it as an LLM proof.