korrents

korrents · papers

From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier (with 18 co-authors)

Terence Tao · 8 Jul 2026 · arxiv.org ↗

4 korrents from this paper

In plain words

AI systems that check math proofs with computers are great at fixed problems but still cannot discover new theorems or settle open questions the way research mathematicians do. Closing that gap would let them expand mathematical knowledge instead of just rediscovering known results or winning contests. It is a position paper that surveys the field and maps five concrete barriers blocking the shift from solvers to research agents.

Our summary of the paper, not the authors' words — written to be readable without the field's vocabulary, from the stored copy of the paper and nothing else. Drafted with xai:grok-4.5 and checked by a person. The authors' own sentences are the quotes below.

Terence Tao did not write this page.

Every claim below was made in this piece, quoted word for word and numbered in the order the piece makes them, so you can read it there rather than take our word for it. The sentence above each quote is our reading of the claim, not their wording. Each quote was checked against a stored copy of the page at build time; where the two differ, the quote is the fact.

  1. Our reading

    The next advance in AI for mathematics requires shifting from predefined problem-solvers to research agents that address frontier challenges with formal reasoning.

    Their wordsWe 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.
    Interesting

  2. Our reading

    Natural-language LLM mathematical reasoners are fundamentally limited by lacking machine-checkable semantics, which blocks autonomous verification needed for open-ended research.

    Their wordsHowever, 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 [Huang et al., 2025b] and precluding autonomous verification, a prerequisite for tackling open-ended mathematical research.
    Interesting

  3. Our reading

    Current AI4Math systems largely operate as solvers of isolated, well-defined proofs rather than as researchers that expand mathematical knowledge.

    Their wordsDespite 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 boundaries of mathematical knowledge.
    Interesting

  4. Our reading

    AI systems are now capable of meaningful contributions to formal mathematics, not only informal problem-solving.

    Their wordsThese developments inform our position that AI systems are now capable of meaningful contributions to formal mathematics, not merely informal problem-solving.
    Interesting