What I’m saying is that you can’t just trust what the AI says because it produces a Lean artifact.
The statement of the theorem has to be correctly translated from English into Lean code.
It’s like translating user requirements into code. The code could run without bugs but not do what the users want.
The only way to know the AI did it correctly is to check. You can’t just take it at face value.