AI Is Starting to Solve Erdős Problems: Are LLMs Becoming Real Mathematical Researchers?

Yes, LLM-based systems are beginning to do pieces of real mathematical research: they have produced new solutions to some open Erdős problems, including work that mathematicians have taken seriously. But “AI is now a mathematical researcher” is only true if you mean a highly capable, tightly scaffolded researcher that needs a formal verifier, careful problem selection, and humans to establish novelty and significance.

First, what counts as solving an Erdős problem?

Paul Erdős posed an enormous number of questions, mostly in combinatorics and number theory. The modern Erdős Problems Project collects many of them, but its catalogue is not a pristine benchmark suite. Some statements have historical ambiguities. Some problems marked open turned out to have an old solution buried in the literature. And the difficulty range is comically wide: “an Erdős problem” can mean a pleasant exercise, an obscure question nobody got around to publishing on, or a problem that has resisted serious specialists for decades.

That distinction matters because a model rediscovering an existing proof is impressive evidence of capability, but it is not a mathematical discovery. A model finding a gap-free proof of a genuinely open statement is stronger. A model discovering a surprising construction, then helping humans extract a broader theorem or a useful new technique, is stronger again.

This is why the most useful public tracking separates full resolutions, partial results, incorrect arguments, and unverified candidates. It also distinguishes AI as the primary source of an argument from less glamorous—but still valuable—uses such as literature search, formalization, rewriting, and computation.

What changed: the loop got better, not just the chatbot

The important systems are not just prompted with “solve this conjecture” and trusted when they emit LaTex. They run a search loop. The model proposes lemmas, constructions, proof outlines, counterexamples, or formal proof steps. A checker rejects bad branches. The system uses the feedback to try again. That looks much closer to compiling and testing code than to asking a chatbot for an explanation.

Lean is especially important here. Lean is a proof assistant: you state definitions and theorems in a formal language, and its kernel checks every allowed inference. A natural-language proof can hide a quantifier error, quietly invoke a false lemma, or skip the one step that does all the work. A Lean proof cannot get credit until those details type-check.

That changes the division of labor. LLMs are very good at proposing many plausible moves and translating intent into local proof steps. Formal tools are very good at saying “no.” Combining those strengths turns hallucination from a silent failure into a failed build. It doesn’t make the search easy, but it makes success far more trustworthy.

Recent research systems illustrate the shift. One formal-proof-search effort reported autonomously resolving nine of 353 attempted open Erdős problems, while also proving open OEIS conjectures and producing results in other mathematical domains. Google DeepMind has described a separate system, Aletheia, as solving several Erdős problems with varying degrees of autonomy and contributing to follow-on human-AI papers. And OpenAI reported an autonomous resolution of a prominent unit-distance conjecture, with external mathematicians praising the proof’s originality and quality.

Why this is research—and why it still isn’t a replacement researcher

Research is not defined by having a PhD, typing proofs into a document, or getting every first attempt right. At its core, it means producing claims the field did not already know, with enough evidence that other people can build on them. On that definition, a verified, novel proof of an open result is real research output, regardless of whether the first draft came from a person or a model.

But research is also a pipeline, not a final theorem. Someone has to identify a question worth asking, reconstruct the surrounding literature, notice whether an allegedly new solution was known in 1966, decide which definitions are productive, and explain why a result changes anyone’s mental model. Current systems are uneven at all of that.

They are particularly vulnerable to a software-engineering-shaped failure mode: optimizing against the wrong spec. If the problem statement is incomplete, mistranscribed, or subtly weaker than the intended question, an agent can spend a lot of compute proving exactly the wrong theorem. Formal verification proves that the encoded statement follows from the encoded assumptions. It does not prove that those assumptions captured the research question people actually care about.

Nor does a proof assistant establish novelty. Think of Lean as an exceptionally strict CI system for correctness, not as GitHub search, code archaeology, product judgment, and peer review rolled into one. The hard external work remains external.

How to evaluate the next “AI solved open math” claim

You don’t need to read algebraic number theory to avoid getting fooled. Treat a claimed AI discovery like an extraordinary production benchmark result: inspect the task definition, provenance, validation path, and independent reproduction.

1. Check whether the problem was genuinely open at the time of the work. Look for a literature review, not merely a database label.
2. Ask what the AI actually did. Did it suggest a key idea, generate the entire argument, formalize a human proof, or search over a human-designed scaffold? These are different achievements.
3. Look for validation beyond model self-critique. The strongest evidence is a Lean or another proof-assistant formalization, plus review by domain mathematicians.
4. Separate correctness from significance. A short proof of an obscure problem may be fully valid and still not represent a major mathematical advance.
5. Watch for selection effects. A list of wins says little about the thousands of failed, duplicated, malformed, or uninteresting attempts unless the evaluation protocol reports them.

What software engineers should take from this

The near-term lesson is not that you should point a coding agent at unsolved mathematics. It is that LLMs become dramatically more useful when we stop treating their text as the product and start treating it as a proposal inside a verifiable workflow.

In math, the verifier is Lean. In software, it is a combination of type checking, tests, linters, fuzzing, model checking, security scanners, benchmarks, staging environments, and review. The agent’s job is to search a huge space of possible implementations or arguments; the harness’s job is to make wrong answers cheap to reject.

That is also the honest answer to the headline question. LLMs are becoming mathematical researchers in the sense that they can now make nontrivial, sometimes novel contributions to a research program. They are not yet independent researchers in the full social and epistemic sense. The frontier is less “a chatbot becomes Gauss” and more “a capable search system gains enough tools and feedback to turn speculative reasoning into checked knowledge.”