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

Jul 16, 2026

From Solvers to Research argues that current AI for Mathematics systems—especially LLM-driven theorem provers in interactive theorem proving (ITP) environments—excel at proving well-defined problems but fall short for frontier research tasks. Open questions are often under-specified, multi-layered, and require novel, rigorous formal reasoning. The position paper surveys AI4Math methods, including datasets, auto-formalization, and proof synthesis, then analyzes limitations across data, relational structure, exploration, tool ecosystems, and human–AI collaboration, proposing a strategic roadmap to shift systems from solvers to research agents.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages47

Reading Time1 h 58 min

Introduction

From solver-oriented systems to research agents

Collection of Resources

Abstract and overview

Unified analysis and taxonomy

Datasets, auto-formalization, and proof synthesis

arXiv :2607 .07779v 1 [ cs .CL] 8 Jul 2026 From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier Eric Jiang1,∗, Xiao Liang1,∗, Yikai Zhang1, Yingjia Wan1, Mengting Li1, Haikang Deng1, Alexander K Taylor1, Justin Baker1, Rushil Raghavan1, Junyi Zhang1, Ying Nian Wu1, Andrea L. Bertozzi1, Kai-Wei Chang1, Raghu Meka1, Matthew Sottile2, Nanyun Peng1, Amit Sahai1, Terence Tao1, Wei Wang1 1University of California, Los Angeles 2Lawrence Livermore National Laboratory Abstract 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. Collection of Resources 1 Introduction AI for Mathematics (AI4Math) has long been a central and foundational area of machine intelligence, reflecting the long-standing ambition to endow machines with rigorous formal mathematical reasoning capabilities. Early work in this field focused on neural-symbolic methods [282] designed to integrate neural pattern recognition with the structured logic of Interactive Theorem Proving (ITP) systems. These approaches have achieved notable success in high-accuracy proof synthesis within formal environments [274, 18, 124], but often rely on fixed, manually designed heuristics, limiting their scalability and applicability across diverse mathematical domains [1] . Recently, the emergence of Large Language Models (LLMs) has led to remarkable progress in informal mathematical reasoning. Models like DeepSeek-R1 [57] and the o-series [106] have achieved strong performance on numerous benchmarks [164, 97] . However, these LLM reasoners that generate informal reasoning in natural language are fundamentally limited by the lack of precise, machine-checkable semantics, making their outputs prone to hallucinations [103] and precluding autonomous verification, a prerequisite for tackling open-ended mathematical research. To bridge this gap, research has been geared towards LLM-driven formal mathematical reasoning systems. By leveraging ITPs such as Lean [50] for rigorous verification, systems including DeepSeek-Prover [55, 267] and Seed-Prover [34] have set new standards for formal proof generation in competition-level mathemat- ∗ Equal contribution. For M. Sottile, this work was performed under the auspices of the U.S. Department of Energy by Lawrence Livermore National Laboratory under Contract DE-AC52-07NA27344 . ics [305] . In parallel, hybrid approaches [293, 38] that combine LLMs with geometrical deduction engines have surpassed human gold-medal performance on International Mathematical Olympiad (IMO) geometry problems. These advances highlight LLMs’ potential in generating formal proofs across diverse mathematical domains. Despite these strides, we argue that current AI4Math systems still largely operate as solvers, excelling at isolated, well-defined proof generation rather than as researchers capable of expanding the bou

FAQs

为什么现有基于LLM的形式化数学系统在研究前沿任务上仍受限？

因为它们主要擅长在定义良好的问题上生成形式化证明，而研究前沿常涉及开放、欠指定且多层抽象的问题；此外，许多系统缺乏可机检的精确语义，从而难以实现自主验证与真正的研究级探索。

文中提出的核心转变是什么？

从预定义的“problem-solver”转向面向前沿数学的“research agents”，使系统能够以严格形式化推理来应对开放式研究挑战。

本文在工作内容上主要覆盖哪些方面？

围绕AI4Math给出系统综述，涵盖数据集、自动形式化与证明合成，并识别现有系统作为数学研究代理的关键限制，随后提出面向未来的路线图与改进方向。

Jul 16, 2026

Upload by Clementine