4 ms·
That's why OpenAI also published machine-checkable proofs. The process is very, very faintly similar to running a typechecker over your software sources.
by eru 3mo ago
That's why OpenAI also published machine-checkable proofs.
The process is very, very faintly similar to running a typechecker over your software sources.
- parineum 3mo agoThey'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.