If you mean > What is missing is an intelligible proof that human mathematicians can understand and use to advance the aims of mathematics.

Then that is not necessarily subjective either if an AI can produce an actually intelligible proof. The problem is that as mathematicians with PDE expertise have mentioned on Twitter the actual solution seems to devolve into an unreadable mess focusing on irrelevant details after a more readable first few pages in the proof. If it wasn't a Lean compiled proof and presented as a human artifact, it would be hard to assess if the deviser of the solution had any actual understanding of the solution.