Hacker News Reader

Is it a correct answer, though? Even with a Lean proof, someone has to be verify that it proved the right theorem.

Checking that the theorem is what we really want to prove is much much less work than going through the whole proof though.

Oh, absolutely. Just saying there’s something for mathematicians to do before publishing results.