3 ms·
What you describe is Tao's rebuttal of #2. I fully agree with him there. It's his rejection of #1 that makes me sad.
by octoberfranklin 20d ago
What you describe is Tao's rebuttal of #2. I fully agree with him there.
It's his rejection of #1 that makes me sad.
- traject_ 20d agoIf 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.
- grey-area 20d agoWell 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.
- auggierose 20d agoit is not his rejection, this is a guest article written by two other people