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

A new position paper argues that AI for mathematics must shift from solving predefined problems to acting as research agents capable of discovering new theorems and resolving open conjectures. The paper reviews current limitations in datasets, relational structure, mathematical exploration, tool ecosystems, and human-AI collaboration, and outlines a roadmap for future AI4Math systems.

arXiv:2607.07779v1 Announce Type: new 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.