True, but verifying proofs is usually easier (or at least more mechanical) than generating proofs. Personally I think this is the best possible use of AI: to have it generate systems that have verifiable properties in some formalized language. That way we can just come up with the properties we want satisfied (which, granted, is not generally trivial) and use the formalized language to verify that the properties are satisfied in the AI-generated code.