# Mathematics with large language models as provers and verifiers

arXiv: https://arxiv.org/abs/2510.12829 · HTML: https://mlsanity.com/paper/2510.12829/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 16 of its 48 references that are in the map.
- First posted on arXiv 11 Oct 2025.

## Builds on (most cited first, 16 of 16)

- [MathArena: Evaluating LLMs on Uncontaminated Math Competitions](https://mlsanity.com/paper/2505.23281/) (2025)
- [The Prompt Report: A Systematic Survey of Prompt Engineering Techniques](https://mlsanity.com/paper/2406.06608/) (2024)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [Language Model Behavior: A Comprehensive Survey](https://mlsanity.com/paper/2303.11504/) (2023)
- [Michelangelo: Long Context Evaluations Beyond Haystacks via Latent Structure Queries](https://mlsanity.com/paper/2409.12640/) (2024)
- [Lean Copilot: Large Language Models as Copilots for Theorem Proving in Lean](https://mlsanity.com/paper/2404.12534/) (2024)
- [A Practical Survey on Zero-shot Prompt Design for In-context Learning](https://mlsanity.com/paper/2309.13205/) (2023)
- [Large Language Models Pass the Turing Test](https://mlsanity.com/paper/2503.23674/) (2025)
- [A Survey of Automatic Prompt Engineering: An Optimization Perspective](https://mlsanity.com/paper/2502.11560/) (2025)
- [Lyra: Orchestrating Dual Correction in Automated Theorem Proving](https://mlsanity.com/paper/2309.15806/) (2023)
- [DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning](https://mlsanity.com/paper/2505.23754/) (2025)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification](https://mlsanity.com/paper/2506.04592/) (2025)
- [Benchmarking Large Language Models for Math Reasoning Tasks](https://mlsanity.com/paper/2408.10839/) (2024)
- [Prompt Engineering and the Effectiveness of Large Language Models in Enhancing Human Productivity](https://mlsanity.com/paper/2507.18638/) (2025)
- [Six mathematical gems from the history of Distance Geometry](https://mlsanity.com/paper/1502.02816/) (2015)

## Built on by (most cited first, 1 of 1)

- [From Chatbot to Digital Colleague: The Paradigm Shift Toward Persistent Autonomous AI](https://mlsanity.com/paper/2606.14502/) (2026)

## 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].