We are not in the singularity. We currently can only produce reliable code / formalizations that have reliable checkers. If there wasn't an oracle that could tell Claude "yes" or "no," it would not be able to prove anything like this.