Can LLM theorem provers tackle genuinely open-ended research problems?

The position paper argues that llm-driven theorem provers still largely operate as solvers. They are "excelling at isolated, well-defined proof generation" but are not yet researchers "capable of expanding the boundaries of mathematical knowledge." The main evidence is the Erdős problems. Recent systems claim to solve some of them, but the authors note that these solutions "are largely obtained from rediscovering results already present in the literature," and the systems still cannot address problems such as the Millennium Prize Problems, which "demand genuinely novel ideas." The proofs in these systems are checked by Lean, a proof assistant, so they are verified in that narrow sense.

The excerpt separates two properties that are easy to run together. A formal proof is verified when the proof assistant accepts it. It is faithful when the formal statement says what the mathematician meant, and the checker does not test that. The excerpt places autoformalization at the point where the two come apart: human mathematics leaves context implicit, so "a single textbook sentence can expand into dozens of lines of formal code," and "successful compilation of a formal statement does not ensure semantic correctness." As its example, HERALD and Kimina-autoformalizer "report comparable headline performance on MiniF2F." Some of the Erdős "solutions" also "resolved misformulated versions of problems rather than the intended mathematical claims."

Against the nearest notes, this excerpt bears on three. Its autoformalization gap limits Can we automatically generate formal verifiers from policy text?: a Lean or z3 check on a generated verifier certifies the code, not that it encodes the policy. It also marks where Can symbolic solvers fix how LLMs reason about logic? stops, since the natural-language-to-symbolic translation stays with the LLM, outside the solver's guarantees. The sharpest contrast is Can AI systems improve themselves through trial and error?, which replaces formal proofs with benchmark validation; this paper makes autonomous verification a prerequisite for open-ended mathematical research. Its account of successes, short proofs once the key insight is found, fits Do language models fail at reasoning due to complexity or novelty?, though the excerpt does not cite that link.

The excerpt does not establish how often these systems succeed. The authors say so: "strong selection bias exists: unsuccessful attempts are rarely reported, so success rates cannot be inferred." The rediscovery claim rests on a citation, [66], that the excerpt does not reproduce, so the literature check cannot be audited here. The five pillars are a roadmap, not evidence that research agents work. Nor does the excerpt address understood, meaning whether a person can follow why a verified proof works; section 5.5 on human–AI collaboration is named but not included. At the strength the evidence allows, the faithfulness point is the best supported, because it concerns what a checker can and cannot certify. The claim that current systems are solvers rather than researchers is a reasoned case built from selected examples, not a measured finding.