Remix clone Hacker News

new | show | ask | jobs Github

▲

UltraSane 5 hours ago

What a ridiculous thing to say. If it was verified in Lean we could be much more confident the proof is correct.

▲

varjag 5 hours ago | parent [-]

It's not a long proof (it's not in Lean after all) so easy enough to comb through for a domain expert.

▲

UltraSane 5 hours ago | parent [-]

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 4 hours ago | parent [-]

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 3 hours ago | parent [-]

One requires you to trust a human and the other requires you to trust mathematics.

	▲	varjag 3 hours ago \| parent [-]
		Let 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?