3 ms·
It's not a long proof (it's not in Lean after all) so easy enough to comb through for a domain expert.
by varjag 3mo ago
It's not a long proof (it's not in Lean after all) so easy enough to comb through for a domain expert.
- UltraSane 3mo agoIf 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 3mo agoHow 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 3mo agoOne requires you to trust a human and the other requires you to trust mathematics.
- varjag 3mo agoLet me simplify it for the sake of argument. Imagine I am unable to follow a middle school proof of Pythagoras. How does it matter if I trust anyone beyond that? What possible contribution can I build on top of that?