Came here to say this. What AI is doing with math is essentially fuzzing, but looking for valid inputs that solve a problem and the inputs are mathematical abstractions. It's a cool approach, but AI doesn't understand what's going on, and without understanding it won't be able to create the next generation of mathematical abstractions needed for the next generation of proofs.