Perhaps I'm missing it, but the "solving" of mathematics seems much more related to computational capacity growth and the development of Lean than necessarily advances in LLMs. Swap the LLM for an RNG and insert unlimited sampling. Don't we get the same result thanks to Lean?