Comment by asib
11 hours 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.
All 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.
So there is no getting around the fact that someone has to verify something. my point still stands.