mlsanityData to 7 Oct 2026

Mathematics with large language models as provers and verifiers

arXiv 2510.12829 ↗First posted 11 Oct 2025cs.CL cs.AI cs.LGcited by 0

Not on the map. Why?

Abstract (arXiv)

During 2024 and 2025 the discussion about the theorem-proving capabilities of large language models started reporting interesting success stories, mostly to do with difficult exercises (such as problems from the International Mathematical Olympiad), but also with conjectures [Feldman & Karbasi, arXiv:2509.18383v1] formulated for the purpose of verifying whether the artificial intelligence could prove it. In this paper we report a theorem proving feat achieved by ChatGPT by using a protocol involving different prover and verifier instances of the gpt-5 model working collaboratively. To make sure that the produced proofs do not suffer from hallucinations, the final proof is formally verified by the lean proof assistant, and the conformance of premises and conclusion of the lean code is verified by a human. Our methodology is by no means complete or exact. It was nonetheless able to solve five out of six 2025 IMO problems, and close about a third of the sixty-six number theory conjectures in [Cohen, Journal of Integer Sequences, 2025].

Key facts. No citing papers in the map yet (data through 7 Oct 2026). Builds on 16 of its 48 references that are in the map. First posted on arXiv 11 Oct 2025.

Builds on

16 of 48 references.

References · 16

  1. 2025MathArena: Evaluating LLMs on Uncontaminated Math Competitionscited by 275
  2. 2024The Prompt Report: A Systematic Survey of Prompt Engineering Techniquescited by 115
  3. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 96
  4. 2023Language Model Behavior: A Comprehensive Surveycited by 92
  5. 2024Michelangelo: Long Context Evaluations Beyond Haystacks via Latent Structure Queriescited by 85
  6. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  7. 2023A Practical Survey on Zero-shot Prompt Design for In-context Learningcited by 49
  8. 2025Large Language Models Pass the Turing Testcited by 48
  9. 2025A Survey of Automatic Prompt Engineering: An Optimization Perspectivecited by 41
  10. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 24
  11. 2025DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learningcited by 23
  12. 2025Autoformalization in the Era of Large Language Models: A Surveycited by 19
4 more
  1. 2025Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verificationcited by 16
  2. 2024Benchmarking Large Language Models for Math Reasoning Taskscited by 12
  3. 2025Prompt Engineering and the Effectiveness of Large Language Models in Enhancing Human Productivitycited by 2
  4. 2015Six mathematical gems from the history of Distance Geometrycited by 1

Built on by

Not cited yet.