Probably an AI-written Lean proof is very different to how a human would write it, and some may say it's more like mathy neuralese. For sure it works but it is not human-friendly and needs to be transformed into something more readable and digestible to be able to extract insights from it.

Not that different from when trying to read an out-of-control vibe coded codebases, or an sloppy AI long email that someone may send you at 9 AM.

Because the problem has almost no value unto itself. The clay statement of navier stokes is not relevant to how CFD is done in practice.

It's about what is non verifiable versus verifiable. The same way it produces "slop" code (which, if you give it test cases, will be 100% correct), it also produces "slop" math.

Code that serves a business function, it's ok if its slop. Math that serves directly a business function also can be slop.

But most open problems are not directly for a particular usecase. People agree widely to attack it due to the perceived possibility of encountering useful mathematical objects along the way, that will then expand the world's mathematical toolset. This is not something that you can easily express in a verifier, and is thus something that is hard to force an LLM system to do.

You are right in that understanding it retrospectively is possible, but that is not going to be as useful as the desired "elegant" objects that expand and unify mathematics. You can't represent these concepts in verifiers.

Again, if you let AI rip at something like say "beat shannon capacity" and suppose it comes up with MIMO as paulraj did, great! It's useful and you can retrospectively understand it, say by expanding shannon to multiple dimensions, as foschini and telatar did. But most math problems are not in that category.

The question then is, if AI is really good at this type of math, how much of the existing mathematical community+process is necessary? I think it will still be necessary, just maybe in fewer cases. Wherever the primary purpose of the math is in a domain and that domain has a verifiable target, we can directly optimise it to that verifiable target in-domain rather than reach for the mathematical community. How well will this work? We'll see. It's not clear if it's even possible to represent most problems this way.