Comment by pfdietz 18 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 17 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 15 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 16 hours ago The proof was of such complexity and length there were lingering doubts. This dispels them. curt15 17 hours ago More so if Lean uncovers logical errors. Note also there is already an ongoing 2nd generation proof. cubefox 15 hours ago I suppose this is the longest Lean proof by a wide margin. pfdietz 14 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 13 hours ago I wonder whether humans could have realistically finished it without AI by 2100. 2 replies → claudismusa 11 hours ago I used to take mathematicians seriously. gggg_g_g__g 12 hours ago Holy shit.
bwestergard 17 hours ago Is that going to be mathematically useful? sebzim4500 17 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 15 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 16 hours ago The proof was of such complexity and length there were lingering doubts. This dispels them. curt15 17 hours ago More so if Lean uncovers logical errors. Note also there is already an ongoing 2nd generation proof.
sebzim4500 17 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 15 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 15 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 16 hours ago The proof was of such complexity and length there were lingering doubts. This dispels them.
curt15 17 hours ago More so if Lean uncovers logical errors. Note also there is already an ongoing 2nd generation proof.
cubefox 15 hours ago I suppose this is the longest Lean proof by a wide margin. pfdietz 14 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 13 hours ago I wonder whether humans could have realistically finished it without AI by 2100. 2 replies →
pfdietz 14 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 13 hours ago I wonder whether humans could have realistically finished it without AI by 2100. 2 replies →
cubefox 13 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.