Terence Tao co-authors paper on LLMs for frontier math research

A landmark position paper published on arXiv (2607.07779) by a team of 18 authors including celebrated mathematician Terence Tao argues that the next leap in AI for Mathematics (AI4Math) requires a decisive shift from current LLM-driven theorem provers — which excel at formal proof generation for well-defined problems — to research agents capable of tackling frontier mathematical challenges. These challenges are often open-ended, under-specified, and involve multiple layers of abstraction, such as discovering new theorems or resolving open conjectures. The paper provides a systematic review of the field, covering datasets, auto-formalization, and proof synthesis, but its core contribution is identifying the fundamental limitations of existing systems in serving as mathematical research agents.

The authors examine critical gaps across five dimensions: datasets, relational structure, mathematical exploration, tool ecosystem, and human-AI collaboration. They argue that current benchmarks and training data fail to capture the exploratory and creative nature of real mathematical research, while existing AI systems lack the ability to navigate the rich relational structure of mathematical knowledge — such as connections between lemmas, definitions, and proofs across different areas. The paper also highlights the need for improved tool ecosystems that integrate formal verification environments (like Lean or Isabelle) with AI agents, and for better human-AI collaboration paradigms where mathematicians can guide and interact with the system iteratively. The roadmap outlined in the paper points toward building autonomous agents that can hypothesize, test, and refine ideas — effectively moving from solvers to research partners.