LLMs prove theorems but do not discover mathematics: researchers outline the next step

A group of researchers published a position paper on arXiv in early July 2026 that systematized the achievements of LLM-theorem provers and identified their fundamental limitation: current systems prove theorems but are incapable of discovering mathematics — and proposed a strategic roadmap for transitioning to full-fledged research agents.

What AI4Math Systems Can Do Today

Over the past several years, LLM systems for formal mathematics have achieved tangible progress. Working with languages for interactive theorem proving (ITP) — primarily Lean 4, Isabelle, and Coq — they have learned to generate formal proofs for well-defined problems. These languages allow proofs to be written so that a computer can mechanically verify each step — making the result fundamentally more reliable than traditional handwritten proofs.

The authors systematized three key directions of development in the field:

• Datasets — corpora of formalized problems have accumulated, ranging from high school to university level, allowing models to be trained on examples of correct proofs
• Autoformalisation — models have improved at translating problem statements written in natural language into strict formal ITP syntax
• Proof synthesis — systems are increasingly confident in finding step-by-step proofs when given a clear initial formulation

All these achievements share one feature: they work only on well-defined, pre-formulated problems. The model knows exactly what must be proven — and searches for the path to that goal.

Why This Is Not Yet Science

True mathematical science is fundamentally different from solving problem sets. It requires the ability to formulate hypotheses, identify unexpected connections between different domains, and attack open problems — often long-standing, poorly formulated, and requiring multiple levels of abstraction. This is precisely where current LLM systems demonstrate systemic limitations.

The authors identify five key problems:

• Data: datasets do not contain examples of how new theorems are born — only solutions to already-posed problems
• Structure: mathematics relies on complex hierarchies of concepts and implicit dependencies between branches, which LLMs poorly assimilate
• Exploration: models can answer questions but cannot formulate new ones — yet this lies at the foundation of science
• Tools: there is no integration with computer algebra systems and specialized mathematical databases
• Collaboration: models cannot be full collaborators — they do not understand the informal context that scientists convey to one another

"The next breakthrough in AI4Math requires a decisive shift from

solvers of predetermined tasks to research agents capable of working at the frontier of mathematics" — the paper's key thesis.

What the Next System Should Be

The strategic roadmap described in the paper envisions a transition to mathematical research agents — systems capable of independently formulating hypotheses, planning research programs, interacting with scientists in a dialogue mode, and iteratively refining problem formulations.

This will require simultaneous development of several directions: new datasets with examples of real discoveries, methods for working with relational structures of mathematics, more mature tool ecosystems, and fundamentally different models of human-machine collaboration. None of these components yet exists in the necessary form — making the task large-scale but clearly formulated.

What This Means

The paper signals an important shift in the AI4Math horizon: from systems for proof verification to systems capable of participating in the discovery of new mathematics. This transition requires fundamentally different architecture than scaling existing approaches. If the proposed roadmap is realized, mathematics may become one of the first fields where AI becomes a true research partner to the scientist.