← Back to context Comment by pfdietz 17 hours ago The formalization is 43.1M lines of Lean. 18 comments pfdietz Reply bwestergard 17 hours ago Is that going to be mathematically useful? sebzim4500 16 hours ago It'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. cvoss 12 hours ago Indeed, this formalization effort spotted a flawed argument in one of the original publications and worked around it to repair the result. Panoramix 14 hours ago How do we know the formalization itself doesn't have any errors? AFAIK it's very far from trivial to formalize something. 4 replies → pfdietz 15 hours ago The proof was of such complexity and length there were lingering doubts. This dispels them. curt15 16 hours ago More so if Lean uncovers logical errors. Note also there is already an ongoing 2nd generation proof. cubefox 14 hours ago I suppose this is the longest Lean proof by a wide margin. pfdietz 13 hours ago It's possibly the longest open source project of any kind (depending on whether you count comments and white space in Linux). cubefox 12 hours ago I wonder whether humans could have realistically finished it without AI by 2100. 2 replies → claudismusa 10 hours ago I used to take mathematicians seriously. gggg_g_g__g 11 hours ago Holy shit.
bwestergard 17 hours ago Is that going to be mathematically useful? sebzim4500 16 hours ago It'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. cvoss 12 hours ago Indeed, this formalization effort spotted a flawed argument in one of the original publications and worked around it to repair the result. Panoramix 14 hours ago How do we know the formalization itself doesn't have any errors? AFAIK it's very far from trivial to formalize something. 4 replies → pfdietz 15 hours ago The proof was of such complexity and length there were lingering doubts. This dispels them. curt15 16 hours ago More so if Lean uncovers logical errors. Note also there is already an ongoing 2nd generation proof.
sebzim4500 16 hours ago It'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. cvoss 12 hours ago Indeed, this formalization effort spotted a flawed argument in one of the original publications and worked around it to repair the result. Panoramix 14 hours ago How do we know the formalization itself doesn't have any errors? AFAIK it's very far from trivial to formalize something. 4 replies →
cvoss 12 hours ago Indeed, this formalization effort spotted a flawed argument in one of the original publications and worked around it to repair the result.
Panoramix 14 hours ago How do we know the formalization itself doesn't have any errors? AFAIK it's very far from trivial to formalize something. 4 replies →
pfdietz 15 hours ago The proof was of such complexity and length there were lingering doubts. This dispels them.
curt15 16 hours ago More so if Lean uncovers logical errors. Note also there is already an ongoing 2nd generation proof.
cubefox 14 hours ago I suppose this is the longest Lean proof by a wide margin. pfdietz 13 hours ago It's possibly the longest open source project of any kind (depending on whether you count comments and white space in Linux). cubefox 12 hours ago I wonder whether humans could have realistically finished it without AI by 2100. 2 replies →
pfdietz 13 hours ago It's possibly the longest open source project of any kind (depending on whether you count comments and white space in Linux). cubefox 12 hours ago I wonder whether humans could have realistically finished it without AI by 2100. 2 replies →
cubefox 12 hours ago I wonder whether humans could have realistically finished it without AI by 2100. 2 replies →
Is that going to be mathematically useful?
It'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.
Indeed, this formalization effort spotted a flawed argument in one of the original publications and worked around it to repair the result.
How do we know the formalization itself doesn't have any errors? AFAIK it's very far from trivial to formalize something.
4 replies →
The proof was of such complexity and length there were lingering doubts. This dispels them.
More so if Lean uncovers logical errors. Note also there is already an ongoing 2nd generation proof.
I suppose this is the longest Lean proof by a wide margin.
It's possibly the longest open source project of any kind (depending on whether you count comments and white space in Linux).
I wonder whether humans could have realistically finished it without AI by 2100.
2 replies →
I used to take mathematicians seriously.
Holy shit.