3 ms·
They're publishing machine checkable proofs because that's the only way they, themselves, can check them. They don't understand the math either.
by parineum 3mo ago
They're publishing machine checkable proofs because that's the only way they, themselves, can check them.
They don't understand the math either.
- inigyou 3mo agoFor 3.5 days we had a machine checkable proof the Collatz conjecture was false. There turned out to be a bug in the machine checker.
- eru 3mo agoYes, however any LLM agent you asked about that proof could tell you that. (And even most humans who know a little bit about the bug.) You are right that Lean isn't great in this respect, and people are working on proof formalisations that are less prone to bugs.