3 ms·

Why is it strange? Are you familiar with how unsupervised proofs are made? It’s basically iterating on Lean code, even if it were able to explain the code to hu

Why is it strange? Are you familiar with how unsupervised proofs are made? It’s basically iterating on Lean code, even if it were able to explain the code to humans it doesn’t mean it can extract actual understanding and structure from it. The papers being outputted by these approaches are nowhere close to being understandable, much less useful. > If the AI can digest it better, then academic mathematicians will become humanities professors Cool, then once that happens we can discuss what to do. In the meantime, AI does not digest proofs properly, does not explain them and does not generate any understanding, and it doesn’t look like that’s going to change. Hence the letter and the criticism made to the approach taken by AI labs. It is not that hard to understand.

bonoboTP 21d ago
I find these discussions pointless. It's like complaining that diffusion models make hands with the wrong finger counts. Yes there was a year or a few months when that was a legit complaint. The phase where AI proves Millennium Prize level problems but can't write up a human-like paper explaining the proof strategy may be similarly brief. It feels pointless to build a grand theory of what AI can fundamentally do in the space of math proofs based on a few months of existence of such strength models. I find it interesting how many people are incapable of imagining that the tech capability will not be frozen at today's level and where we were e.g. a year ago and that a similar change may happen until next year. Instead they make sweeping assumptions that the current limitations will be with us for our lifetimes. You need a much stronger way to adapt to the new reality.
- gjulianm 21d ago
  > The phase where AI proves Millennium Prize level problems but can't write up a human-like paper explaining the proof strategy may be similarly brief It's absurd to assume that because LLMs are improving in certain aspects they will improve in everything, specially when the part they are lacking in is not precisely something that would be a strength of their architecture. I mean, models have improved a lot but they are still not good at strictly following instructions consistently (there's a reason why AI labs are worried about safety alignment). They are still mediocre to bad at software design, even the latest models (haven't tested Astra seriously yet). And it's the same reason they are bad at creating mathematical theories: they do not have mental models like we do, it's not even useful for them. Their comprehension is limited to textual context that they need to refresh and reprocess continuously. That's just how LLMs work. > I find it interesting how many people are incapable of imagining that the tech capability will not be frozen I find it interesting that after taking this long to, I assume, finally understanding the point the letter was making, you automatically switch to "oh well AI will do that too".

bonoboTP 21d ago

I find these discussions pointless. It's like complaining that diffusion models make hands with the wrong finger counts. Yes there was a year or a few months when that was a legit complaint. The phase where AI proves Millennium Prize level problems but can't write up a human-like paper explaining the proof strategy may be similarly brief. It feels pointless to build a grand theory of what AI can fundamentally do in the space of math proofs based on a few months of existence of such strength models. I find it interesting how many people are incapable of imagining that the tech capability will not be frozen at today's level and where we were e.g. a year ago and that a similar change may happen until next year. Instead they make sweeping assumptions that the current limitations will be with us for our lifetimes. You need a much stronger way to adapt to the new reality.

gjulianm 21d ago
> The phase where AI proves Millennium Prize level problems but can't write up a human-like paper explaining the proof strategy may be similarly brief It's absurd to assume that because LLMs are improving in certain aspects they will improve in everything, specially when the part they are lacking in is not precisely something that would be a strength of their architecture. I mean, models have improved a lot but they are still not good at strictly following instructions consistently (there's a reason why AI labs are worried about safety alignment). They are still mediocre to bad at software design, even the latest models (haven't tested Astra seriously yet). And it's the same reason they are bad at creating mathematical theories: they do not have mental models like we do, it's not even useful for them. Their comprehension is limited to textual context that they need to refresh and reprocess continuously. That's just how LLMs work. > I find it interesting how many people are incapable of imagining that the tech capability will not be frozen I find it interesting that after taking this long to, I assume, finally understanding the point the letter was making, you automatically switch to "oh well AI will do that too".