Comment by snthpy

How does a sign error pass a Lean proof?

If it doesn't have a Lean proof, why would we bother with it? And they really shouldn't publish it! We don't need math slop too.