| ▲ | kmeisthax 4 hours 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 3 hours ago | parent [-] | |
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. | ||