Thread

To grieve, or not to grieve?

167 points · 156 comments · stabbles

piker · 1790935948 · focus · HN ↗
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?
1. azan_ · 1790937598 · focus · HN ↗
  Absolutely not. The search space is basically infinite.
  1. piker · 1790938062 · focus · HN ↗
    Right, but without Lean the "insert unlimited sampling" doesn't work.

Unofficial Hacker News client; not affiliated with Y Combinator.