Hacker News Reader

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.

View on HN

the autoformalization could be proving a subtly distinct result; if the area is not in mathlib already there's likely not a good reference theorem specification to use for a comparator check. or it could be exploiting kernel bugs. just using a second checker kernel is not enough; there has been an example of a model interpolating bugs across multiple checkers in a single bogus proof.

Reply on news.ycombinator.com