openai has retracted many of their lean proofs for the big drop of supposed novel mathematical solns. if frontier ai screws it up , how does this inconsistency manifest in weaker models?