alt Hacker NewsIt's nice to know that they didn't miss anything. The natural language proof is 10,000 pages and they have missed groups in the past.
Replies
Panoramix • yesterday at 7:16 PM
How do we know the formalization itself doesn't have any errors? AFAIK it's very far from trivial to formalize something.
➕ show 2 replies
Indeed, this formalization effort spotted a flawed argument in one of the original publications and worked around it to repair the result.