FWIW this is my understanding of his argument and I am not a mathematician.
As Tao points out, merely suggesting new open questions isn't really sufficient. Part of what gives these problems their fame is their notoriety, their difficulty, the fact that many prodigious mathematicians have spent an evening or week or month or several years studying it.
It wouldn't be as interesting if it had just been solved by the fifth random mathematician who considered it
Notably, gardening a new field of study in math is somewhat nontrivial. You have to introduce the field, illustrate some relevance or connections, and then - and this is key - not solve all of the low-hanging fruit yourself! Because you need somebody else to become an expert in that particular field.
The analog in programming is: if a large company merely open sources a product that's decent but not great and in a language nobody wants to maintain, but they don't commit to maintaining it themselves.
Suddenly there's a bit of a vacuum because in order to provide something of value, you either need to:
1. Implement something more complete than was initially open sourced
2. Or maintain something in a horrendous language while incrementally improving it and keeping it relevant
3. Or rewrite it into a tolerable and maintainable modern language.
What the large company has done is create a vacuum in the tool space where you now require extreme motivation to get someone else to step in.
Note that in this scenario, in 2026, it's actually not such a big deal. I think several recent models could happily translate it into a more maintainable language themselves or happily maintain it in the original crufty one. And so the question is: which parts of this analogy are true in math, too?
You're either being intentionally obtuse, or unintentionally ignorant.
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...
Now I wonder if someone could port his proof to Lean
In the case of mathematicians, I think not as researchers. What would a research mathematician do? I don't think there would be any reason to try to gain insight from proofs that AI made for the sake of understanding. I don't see what that would achieve besides just retaining extremely niche knowledge (which AI or the oracle already does). The whole point of having that knowledge was to build toward novel work which the AI/oracle does. Also, the time spent and difficulty understanding them could be very high but with no payoff besides just understanding them because the AI/oracle would be used to solve all the problems anyway.