Comment by UltraSane

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.