No Lean theorem file contains sorry/admit/axiom/constant declarations according to grep audit.
