My claim is that LLMs waste a lot of time training on all available data.
Math is a sequence of formal rules applied to construct a proof tree. Therefore an AI trained on these rules could be far more efficient, and search far deeper into proof space
It has been tried. Lenat's Automated Mathematician, for example. The problem is that the system succumbs to combinatorial explosion, not knowing which directions are interesting/promising/productive. LLMs seem to pick up some kind of intuition from the data they are fed. The generated data might not have the needed "human touch" or whatever it is.
It might just be that we didn't have enough compute till now. StockFish definitely has superior intuition
StockFish amplifies weak "intuition" (heuristic and simple neural estimators) through extensive Alpha-Beta search made possible by the low(ish) branching factor of chess. It doesn't work for Go already (KataGo uses larger neural networks to guide search more efficiently). I doubt either will work for math where branching factor is even bigger and the success criteria (is the result interesting and so on) are not strictly defined.