I think eventually there will be sort of a centralized more or less automated repository for ingesting and sorting ai-generated lean proofs and making them searchable and re-usable. On some level it kind of doesn't matter if mathematicians can ingest the results, if coding agents can just search for them online and use them in their own proofs.

I actually think it would be very smart for the big AI labs to get together to fund an independent organization to manage such a thing, and hire mathematicians to run it.

What is happening now is that some aspects of mathematics are turning into essentially an exercise in software engineering. It is well known that proofs and computer programs have an isomorphism, and I think the eventual merger is more or less inevitable.

That's not to say that there isn't an infinite amount of work remaining for mathematicians to do. There are only so many problems that are going to be amenable to this approach.