6 ms·
To the credit of the original commenter, that is why they said "give it one or two years". _Right now_ we need the experts to formalize/check. They're saying th
by asib 16d ago
To the credit of the original commenter, that is why they said "give it one or two years". _Right now_ we need the experts to formalize/check. They're saying they think LLMs will reach a point in the near future where that won't be necessary.
- pfdietz 16d agoAll we need experts for right now is verifying the formalization of the statement of the problem is correct. The proof itself, that formalization is checked automatically.
- paulpauper 16d agoSo there is no getting around the fact that someone has to verify something. my point still stands.
- pfdietz 16d agoVerify/check something that is orders of magnitude smaller than the proof. It's like reading the abstract vs. reading the paper.