Elamur Research⌕
☰
home / papers / 2026 / Open Problems Solved by LLMs? A Survey of Verifiable Mathematical Discovery

Open Problems Solved by LLMs? A Survey of Verifiable Mathematical Discovery

Paper · 2026 · Ioannis Tzachristas, Georgios Tzachristas and Aifen Sui

Summary

Headlines saying LLMs have "solved open problems" in mathematics are often vague. "Open" can mean an improvable bound, a missing construction or an unproven theorem, and the model rarely works without external tools. This survey offers a framework for judging such claims.

The authors make four contributions:

  • a four-tier evidence ladder that ranks how directly a reader can confirm a reported advance;
  • a map of mathematical areas by difficulty factors such as verifiability, abstraction depth, search structure, formalization cost and training data;
  • a timeline running from transformers and chain-of-thought prompting through tool use to evolutionary search;
  • a reference architecture in which an LLM proposes candidates, executors and verifiers filter them, and an archive feeds later rounds.

Their central conclusion is that credible successes come from domains with cheap but rigorous checkers. Systems design matters more than better free-form reasoning. The paper closes with a reproducibility checklist and rules for handling announcements from social media and wikis. This matters for anyone evaluating or building AI-for-discovery tools.

Key points

  • Evidence tiers. The survey covers only tiers A–C.
    • A: proof checked in Lean, Coq or Isabelle.
    • B: machine-checkable certificate with a deterministic checker.
    • C: new best-known result with an open evaluator, baselines and ablations.
    • D: conjectures or partial progress, not counted as "solved".
  • Case studies and their tiers:
    • FunSearch and AlphaEvolve: tier C.
    • AlphaGeometry: tier B/C.
    • Gilbert–Pollak Steiner-ratio lower bound (Ke et al., 2026): tier B.
    • Erdős Problem #728, a Lean proof attributed to GPT-5.2 Pro + Aristotle: tier A.
    • Knuth's "Claude's Cycles", a Hamiltonian-cycle decomposition of a directed toroidal grid: tier A/B.
  • Verifier spectrum. Heuristic tests are cheap but noisy, and proof assistants are rigorous but costly. Certificates with deterministic checkers are the current sweet spot. SMT and LTL solvers are proposed as a scalable middle layer.
  • Community signals. Posts on Mathstodon, Hacker News or LinkedIn and Erdős-wiki labels (full/partial/incorrect) stay at tier D unless they link to a checker, proof or citable artifact.
  • Reproducibility checklist. Reports should include:
    • the prior baseline;
    • full verifier code;
    • the resulting artifacts;
    • the compute budget (evaluations, LLM calls, wall-clock time);
    • reruns with different seeds and leakage checks;
    • disclosure of manual human steps.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Technical University of MunichMunich · Germany62 works · 48,970 citations🎓National Technical University of AthensAthens · Greece8 works · 461 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 worksComputational Theory and Mathematics · 321 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,685 works

Cite

Cite as Ioannis Tzachristas, Georgios Tzachristas and Aifen Sui. 2026. Open Problems Solved by LLMs? A Survey of Verifiable Mathematical Discovery. Proceedings of The Big Picture v2: Crafting a Research Narrative.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2026.bigpicture-main.2

@inproceedings{tzachristas2026open,
  title = {{Open Problems Solved by LLMs? A Survey of Verifiable Mathematical Discovery}},
  author = {Ioannis Tzachristas, Georgios Tzachristas and Aifen Sui},
  booktitle = {Proceedings of The Big Picture v2: Crafting a Research Narrative},
  year = {2026},
  doi = {10.18653/v1/2026.bigpicture-main.2},
  url = {https://doi.org/10.18653/v1/2026.bigpicture-main.2}
}

References

28 references, 11 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Hacker News contributors. 2026. Erdős problem \#728 was solved more or less autonomously by GPT-5.2 Pro. Hacker News discussion thread. Accessed May 12, 2026. find
  2. Zhangir Azerbayev, Bartosz Piotrowski, Hailey Schoelkopf, Edward W. Ayers, Dragomir Radev, and Jeremy Avigad. 2023a. ProofNet: Autoformalizing and formally proving undergraduate-level mathematics. CoRR, abs/2302.12433.
  3. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021. Measuring mathematical problem solving with the MATH dataset. CoRR, abs/2103.03874.
  4. Zhangir Azerbayev, Hailey Schoelkopf, Keiran Paster, Marco Dos Santos, Stephen McAleer, Albert Q. Jiang, Jia Deng, Stella Biderman, and Sean Welleck. 2023b. Llemma: An open language model for mathematics. CoRR, abs/2310.10631.
  5. Torsten Hoefler. 2026. Knuth’s AI breakthrough: Claude Opus 4.6 solved open math problem. LinkedIn post. Accessed May 12, 2026. find
  6. Clark Barrett and Cesare Tinelli. 2018. Satisfiability modulo theories. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 305–343. Springer. find
  7. Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z. Horváth, Goran Žužić, Eric Wieser, Aja Huang, Julian Schrittwieser, et al. 2026. Olympiad-level formal mathematical reasoning with reinforcement learning. Nature, 651:607–613. find
  8. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. 1999. Symbolic model checking without BDDs. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1579 of Lecture Notes in Computer Science, pages 193–207. Springer. find
  9. Yisi Ke, Tianyu Huang, Yankai Shu, Di He, Jingchu Gai, and Liwei Wang. 2026. Towards solving the Gilbert–Pollak conjecture via large language models. CoRR, abs/2601.22365. — [arXiv:2601.22365](https://arxiv.org/abs/2601.22365) find
  10. Joseph Boland. 2026. ChatGPT 5.2 solves Erdos \#728 with Terence Tao. LinkedIn post. Accessed May 12, 2026. find
  11. Donald E. Knuth. 2026. Claude’s Cycles. Stanford Computer Science technical note. Revised Apr. 14, 2026; accessed May 12, 2026. find
  12. Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D. Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. 2020. Language models are few-shot learners. Advances in Neural Information Processing Systems, 33.
  13. Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. 2022. HyperTree Proof Search for neural theorem proving. CoRR, abs/2205.11491.
  14. Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. 2021. Training verifiers to solve math word problems. CoRR, abs/2110.14168.
  15. Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. 2022. Solving quantitative reasoning problems with language models. CoRR, abs/2206.14…
  16. Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of Lecture Notes in Computer Science, pages 337–340. Springer. find
  17. Kim Morrison and contributors. 2026. KnuthClaude-Lean: Lean 4 formalization of Knuth’s “Claude’s Cycles”. GitHub repository. Accessed May 12, 2026. find
  18. Alexander Novikov, Ngan Vu, Marvin Eisenberger, Emilien Dupont, Po-Sen Huang, Adam Zsolt Wagner, Sergey Shirobokov, Borislav Kozlovskii, Francisco J. R. Ruiz, Abbas Mehrabian, M. Pawan Kumar, Abigail See, Swarat Chaudhuri, George Holland, Alex Davies, Sebastian Nowozin, Pushmeet Kohli, and Matej Bal… — AlphaEvolve: A coding agent for scientific and algorithmic discovery
  19. Jordan S. Ellenberg, Cristofero S. Fraser-Taliente, Thomas R. Harvey, Karan Srivastava, and Andrew V. Sutherland. 2025. Generative modeling for mathematical discovery. CoRR, abs/2503.11061. — [arXiv:2503.11061](https://arxiv.org/abs/2503.11061) find
  20. Erdős Problems community. 2026. 728 discussion thread. Erdős Problems forum thread. Accessed May 12, 2026. find
  21. Bogdan Georgiev, Javier Gómez-Serrano, Terence Tao, and Adam Zsolt Wagner. 2025. Mathematical exploration and discovery at scale. CoRR, abs/2511.02864. find
  22. OpenAI. 2025. Advancing science and math with GPT-5.2. OpenAI blog. Accessed May 12, 2026. find
  23. Edgar N. Gilbert and Henry O. Pollak. 1968. Steiner minimal trees. SIAM Journal on Applied Mathematics, 16(1):1–29. find
  24. Amir Pnueli. 1977. The temporal logic of programs. In 18th Annual Symposium on Foundations of Computer Science (FOCS), pages 46–57. find
  25. Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi. 2024. Mathematical discoveries from program search with large language models…
  26. Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik Narasimhan, and Yuan Cao. 2023. ReAct: Synergizing reasoning and acting in language models. In International Conference on Learning Representations.
  27. Mert Yuksekgonul, Daniel Koceja, Xinhao Li, Federico Bianchi, Jed McCaleb, Xiaolong Wang, Jan Kautz, Yejin Choi, James Zou, Carlos Guestrin, and Yu Sun. 2026. Learning to discover at test time. CoRR, abs/2601.16175. find
  28. Timo Schick, Jane Dwivedi-Yu, Roberto Dessì, Roberta Raileanu, Maria Lomeli, Eric Hambro, Luke Zettlemoyer, Nicola Cancedda, and Thomas Scialom. 2023. Toolformer: Language models can teach themselves to use tools. In Advances in Neural Information Processing Systems, volume 36.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/tzachristas-2026-open-problems-solved-llms-survey/