Comment by jaykru

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.