alt Hacker NewsIf 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.
Well perhaps we should use occam’s razor here.
If it doesn’t seem like the lllm understands the proof, it probably doesn’t.
Just because it generated something that works doesn’t mean it understands it, and the evidence from its proof is that it does not, which is not very surprising given the technology we’re talking about, which generates likely phrases based on a corpus and training.