Comment by pama

Not sure why you say that. All the major AI-generated proofs so far were done by AI without using lean, and then later validated by AI formalizing with lean in a separate process. Do you mean we would not have enough rigorous training data perhaps?