Have you tried to read the Lean proofs produced for any of the recent high-profile results? They're extremely long, terribly structured, and don't indicate which parts are restating known results from literature and which are unique to the proof at hand. That's what makes them inscrutable.

It's similar to Mochizuki claiming to have proved the ABC conjecture, with a proof depending on ideas developed over a large number of obscure papers, that required mathematicians to spend a lot of time before they felt they understood it well enough to point out flaws.

If AI solves all famous open problems and the non-famous ones, too, without advances in the readability of their output, there'll still be some work to do to digest and rearrange the proofs for human consumption. During that process, the mathematician may well get some new ideas...