← Back to context Comment by varjag 2 months ago It's not a long proof (it's not in Lean after all) so easy enough to comb through for a domain expert. 4 comments varjag Reply UltraSane 2 months ago If it was in Lean anyone could verify it instantly. That is the huge advantage of it. Manual math Proof verification labor might be the most limited resource ever. varjag 2 months ago How does it matter if it Lean verified or a human verified proof if you comprehend neither?There can't be too many people working in that corner of graph theory, and I expect the result to them being eminently straightforward. jackphilson 2 months ago One requires you to trust a human and the other requires you to trust mathematics. 1 reply →
UltraSane 2 months ago If it was in Lean anyone could verify it instantly. That is the huge advantage of it. Manual math Proof verification labor might be the most limited resource ever. varjag 2 months ago How does it matter if it Lean verified or a human verified proof if you comprehend neither?There can't be too many people working in that corner of graph theory, and I expect the result to them being eminently straightforward. jackphilson 2 months ago One requires you to trust a human and the other requires you to trust mathematics. 1 reply →
varjag 2 months ago How does it matter if it Lean verified or a human verified proof if you comprehend neither?There can't be too many people working in that corner of graph theory, and I expect the result to them being eminently straightforward. jackphilson 2 months ago One requires you to trust a human and the other requires you to trust mathematics. 1 reply →
jackphilson 2 months ago One requires you to trust a human and the other requires you to trust mathematics. 1 reply →
If it was in Lean anyone could verify it instantly. That is the huge advantage of it. Manual math Proof verification labor might be the most limited resource ever.
How does it matter if it Lean verified or a human verified proof if you comprehend neither?
There can't be too many people working in that corner of graph theory, and I expect the result to them being eminently straightforward.
One requires you to trust a human and the other requires you to trust mathematics.
1 reply →