Nice article. I didn't read every section in detail but I think it makes a good point that AI researchers maybe focus too much on the thought of creating new mathematics while being able to repdroduce, index or formalize existing mathematics is really they key goal imo. This will then also lead to new mathematics. I think the more you advance in mathematical maturity the bigger the "brush" becomes with which you make your strokes. As an undergrad a stroke can be a single argument in a proof, or a simple Lemma. As a professor it can be a good guess for a well-posedness strategy for a PDE. I think AI will help humans find new mathematics with much bigger brush strokes. If you need to generalize a specific inequality on the whole space to Lipschitz domains, perhaps AI will give you a dozen pages, perhaps even of formalized Lean, in a single stroke. If you are a scientist and consider an ODE model, perhaps AI can give you formally verified error and convergence bounds using your specific constants. You switch to a probabilistic setting? Do not worry. All of these are examples of not very deep but tedious and non-trivial mathematical busywork that can take days or weeks. The mathematical ability necessary to do this has in my opinion already been demonstrated by o3 in rare cases. It can not piece things together yet though. But GPT-4 could not piece together proofs to undergrad homework problems while o3 now can. So I believe improvement is quite possible.