LLMs prove theorems but don't discover mathematics: researchers outline the next step

A group of researchers published a position paper on arXiv in early July 2026. It sums up the achievements of LLM theorem provers and identifies their fundamental limit: today's systems prove theorems but cannot discover mathematics. The paper also proposes a strategic roadmap toward full-fledged research agents.

What AI4Math systems can do today

Over a few years, LLM systems for formal mathematics have made tangible progress. Working with interactive theorem proving (ITP) languages, primarily Lean 4, Isabelle and Coq, they have learned to generate formal proofs for well-defined problems. These languages let users write proofs so that a computer can mechanically check every step, which makes the result fundamentally more reliable than traditional handwritten proofs.

The authors group progress in the field into three key areas:

• Datasets: corpora of formalized problems, from school to university level, have been built up and allow models to train on examples of correct proofs
• Autoformalization: models have improved at translating problem statements written in natural language into strict ITP formal syntax
• Proof synthesis: systems are increasingly good at finding step-by-step proofs when given a clear initial statement

All these advances share one trait: they work only on well-defined, pre-formulated problems. The model knows exactly what has to be proved and searches for a path to that goal.

Why this is not yet science

Real mathematical research differs fundamentally from working through a problem set. It requires the ability to formulate conjectures, spot unexpected links between different fields and attack open problems, which are often decades in the making, loosely defined and span several levels of abstraction. This is where current LLM systems show systematic limitations.

The authors single out five key problems:

• Data: datasets contain no examples of how new theorems are born, only solutions to problems that have already been posed
• Structure: mathematics relies on complex hierarchies of concepts and implicit dependencies between branches, which LLMs absorb poorly
• Research: models can answer questions but cannot formulate new ones, which is the foundation of science
• Tools: there is no integration with computer algebra systems or specialized mathematical databases
• Collaboration: models cannot be full co-authors, because they do not grasp the informal context that scientists pass to one another

"The next breakthrough in AI4Math requires a decisive shift from

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

What the next system should look like

The strategic roadmap described in the paper calls for a move toward mathematical research agents: systems able to formulate conjectures on their own, plan a research program, work with scientists in dialogue and iteratively refine the problem statement.

This will require several areas to advance at the same time: new datasets with examples of real discoveries, methods for handling the relational structures of mathematics, more mature tool ecosystems and fundamentally different models of human-machine collaboration. None of these components exists yet in the required form, which makes the task large in scale but clearly defined.

What this means

The paper signals an important shift in the horizon of AI4Math tasks: from systems that verify proofs to systems that can take part in discovering new mathematics. This transition requires a fundamentally different architecture than scaling up existing approaches. If the proposed roadmap is carried out, mathematics may become one of the first fields where AI acts as a genuine research partner to scientists.