> I expect language models to also get crazy good at mathematical theorem proving Indeed, systems like AlphaProof / AlphaGeometry are already able to win a sil

> I expect language models to also get crazy good at mathematical theorem proving Indeed, systems like AlphaProof / AlphaGeometry are already able to win a silver medal at the IMO, and the former relies on Lean for theorem verification [1]. On the open source side, I really like the ideas in LeanDojo [2], which use a form of RAG to assist the LLM with premise selection. [1] https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/ https://deepmind.google/discover/blog/ai-solves-imo-problems... [2] https://leandojo.org/ https://leandojo.org/