LLMs for Mathematics

Stream: Machine Learning for Theorem Proving

[Anh Nguyễn]

Could anyone please tell me about the recent LLMs for mathematics

[Lars Ericson]

https://blog.eleuther.ai/llemma/

https://research.google/blog/minerva-solving-quantitative-reasoning-problems-with-language-models/

https://toloka.ai/blog/u-math/

[Notification Bot]

A message was moved here from #Machine Learning for Theorem Proving > Simple but hard puzzler for LLMs by Jason Rute.

[Notification Bot]

A message was moved here from #Machine Learning for Theorem Proving > Simple but hard puzzler for LLMs by Jason Rute.

[Jason Rute]

@Anh Nguyễn This is much too vague a question. For one there is a lot of stuff out there. For another, the field is rapidly evolving. If you mean LLMs for formal math like Lean, Coq, Isabelle, you may want to see this survey article. https://arxiv.org/abs/2412.16075

For informal math, there are recent models like o1, o3, QWQ, DeepSeek-R1, and Gemini Flash Thinking. Many are free to use (or at least some versions are free to use).

[Ralph Furman]

To add to the informal side, you can try all of those models side by side for free at sugaku, eg: https://sugaku.net/qna/5afa266a-7fb5-4475-af9d-3d2b021d5c67/