mlsanityData to 7 Oct 2026

From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

arXiv 2607.07779 ↗First posted 8 Jul 2026cs.CL cs.AIcited by 1

Not on the map. Why?

Abstract (arXiv)

Recent developments in AI for Mathematics (AI4Math), especially Large Language Model (LLM)-driven theorem provers, has achieved remarkable success in formal proof generation for well-defined mathematical problems through Interactive Theorem Proving (ITP) languages. However, current systems remain fundamentally limited in tackling frontier research mathematics, such as discovering new theorems or resolving open conjectures, which are often open-ended, under-specified, and involve multiple layers of abstraction. We argue that the next leap in AI4Math systems requires a decisive shift from predefined problem-solvers to research agents that can address frontier mathematical challenges with rigorous formal mathematical reasoning. In this position paper, we provide a systematic review of the field, covering datasets, auto-formalization, and proof synthesis. More importantly, we identify core limitations of existing systems in serving as mathematical research agents, examining issues across datasets, relational structure, mathematical exploration, tool ecosystem, and human-AI collaboration, outlining a strategic road-map for the future of AI4Math.

Key facts. Cited by 1 paper in the map (data through 7 Oct 2026). Builds on 194 of its 292 references that are in the map. First posted on arXiv 8 Jul 2026.

Builds on

194 of 292 references.

References · 194

  1. 2023GPT-4 Technical Reportcited by 18,132
  2. 2022Training language models to follow instructions with human feedbackcited by 15,712
  3. 2017Proximal Policy Optimization Algorithmscited by 14,441
  4. 2024The Llama 3 Herd of Modelscited by 14,192
  5. 2023Llama 2: Open Foundation and Fine-Tuned Chat Modelscited by 12,865
  6. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,302
  7. 2021Training Verifiers to Solve Math Word Problemscited by 9,743
  8. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 8,851
  9. 2022ReAct: Synergizing Reasoning and Acting in Language Modelscited by 8,355
  10. 2025Qwen3 Technical Reportcited by 8,195
  11. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  12. 2020Measuring Massive Multitask Language Understandingcited by 7,768
38 more
  1. 2022Self-Consistency Improves Chain of Thought Reasoning in Language Modelscited by 5,601
  2. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  3. 2024Qwen2.5 Technical Reportcited by 4,713
  4. 2018Think you have Solved Question Answering? Try ARC, the AI2 Reasoning Challengecited by 4,710
  5. 2022Large Language Models are Zero-Shot Reasonerscited by 4,323
  6. 2023Toolformer: Language Models Can Teach Themselves to Use Toolscited by 4,072
  7. 2023Reflexion: Language Agents with Verbal Reinforcement Learningcited by 4,064
  8. 2025Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilitiescited by 3,655
  9. 2023Let's Verify Step by Stepcited by 3,598
  10. 2023Self-Refine: Iterative Refinement with Self-Feedbackcited by 3,317
  11. 2024Gemini 1.5: Unlocking multimodal understanding across millions of tokens of contextcited by 3,175
  12. 2023Tree of Thoughts: Deliberate Problem Solving with Large Language Modelscited by 3,155
  13. 2025DAPO: An Open-Source LLM Reinforcement Learning System at Scalecited by 2,678
  14. 2022Language Models (Mostly) Know What They Knowcited by 1,783
  15. 2023MathVista: Evaluating Mathematical Reasoning of Foundation Models in Visual Contextscited by 1,582
  16. 2023A Survey on Hallucination in Large Language Models: Principles, Taxonomy, Challenges, and Open Questionscited by 1,582
  17. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
  18. 2024OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problemscited by 1,099
  19. 2022Program of Thoughts Prompting: Disentangling Computation from Reasoning for Numerical Reasoning Taskscited by 1,057
  20. 2024Qwen2.5-Math Technical Report: Toward Mathematical Expert Model via Self-Improvementcited by 1,057
  21. 2023Teaching Large Language Models to Self-Debugcited by 963
  22. 2022STaR: Bootstrapping Reasoning With Reasoningcited by 895
  23. 2023Math-Shepherd: Verify and Reinforce LLMs Step-by-step without Human Annotationscited by 895
  24. 2023Graph of Thoughts: Solving Elaborate Problems with Large Language Modelscited by 873
  25. 2022Solving math word problems with process- and outcome-based feedbackcited by 871
  26. 2023Reasoning with Language Model is Planning with World Modelcited by 846
  27. 2023Semantic Uncertainty: Linguistic Invariances for Uncertainty Estimation in Natural Language Generationcited by 795
  28. 2025AlphaEvolve: A coding agent for scientific and algorithmic discoverycited by 763
  29. 2023MetaMath: Bootstrap Your Own Mathematical Questions for Large Language Modelscited by 724
  30. 2022Automatic Chain of Thought Prompting in Large Language Modelscited by 684
  31. 2022PAL: Program-aided Language Modelscited by 635
  32. 2023WizardMath: Empowering Mathematical Reasoning for Large Language Models via Reinforced Evol-Instructcited by 618
  33. 2024MathVerse: Does Your Multi-modal LLM Truly See the Diagrams in Visual Math Problems?cited by 573
  34. 2023Language Agent Tree Search Unifies Reasoning Acting and Planning in Language Modelscited by 551
  35. 2023Plan-and-Solve Prompting: Improving Zero-Shot Chain-of-Thought Reasoning by Large Language Modelscited by 550
  36. 2023Reinforced Self-Training (ReST) for Language Modelingcited by 486
  37. 2024Improve Mathematical Reasoning in Language Models by Automated Process Supervisioncited by 426
  38. 2023Scaling Relationship on Learning Mathematical Reasoning with Large Language Modelscited by 417

50 most cited of 194 All 194 (JSON)

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2026: 1.

1 paper.

  1. 2026Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verificationcited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2024Formal Mathematical Reasoning: A New Frontier in AI
  2. 2026Advancing Mathematics Research with AI-Driven Formal Proof Search
  3. 2023math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories
  4. 2026Measuring Progress in Reasoning Toward Mathematical Discovery with Automatic Verification
  5. 2025Autoformalization in the Era of Large Language Models: A Survey
  6. 2026Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
  7. 2026EternalMath: A Living Benchmark of Frontier Mathematics that Evolves with Human Discovery
  8. 2026Prove2Me: An Open Collaborative Platform for Scaling Math Formalization