10 ms·
Keep in mind the last big LLM maths proof (disproving the Collatz conjecture) turned out to just be exploiting five different bugs in LEAN
by kmeisthax 3mo ago
Keep in mind the last big LLM maths proof (disproving the Collatz conjecture) turned out to just be exploiting five different bugs in LEAN
- empath75 3mo agoThat 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.