If it was as simple as that we'd have many more computer-generated proofs than we have now and the Gen AI results would be unremarkable.

Take the Rieman hypothesis. All one would have to do to prove or disprove it would be to encode the statement of the hypothesis in Lean, press enter, and we're off to the races.

That's not how it works. Essentially you have to encode all the intermediary steps of the proof in Lean too, and then Lean can check their correctness for you and check that they lead to each other. But it won't just generate a whole proof from nothing. That is the whole point of the Gen AI math claims.