Comment by piker
6 days ago
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?
Absolutely not. The search space is basically infinite.
Right, but without Lean the "insert unlimited sampling" doesn't work.