More and more cases of AI helping solve previously unsolved mathematical problems are emerging.
In what appears to be a significant milestone, OpenAI’s GPT-5.2 has reportedly solved Erdős problem #728, marking what could be the first instance of AI autonomously resolving an open mathematical conjecture before any human mathematician.
The breakthrough was announced by Cambridge mathematics student AcerFur on X following a collaborative verification effort. The problem, which asks about the existence of infinitely many integers a, b, n satisfying specific divisibility and inequality conditions involving factorials, had remained unsolved since it was first posed. Specifically, the problem asks: “Let C>0 and ϵ>0 be sufficiently small. Are there infinitely many integers a,b,n with a≥ϵn and b≥ϵn such that a!b!∣n!(a+b−n)! and a+b>n+Clogn?”
According to AcerFur’s account, GPT-5.2 generated the initial solution and proof, which was then validated by Harmonic’s Aristotle system using formal verification in Lean, a proof assistant that provides machine-checkable guarantees of correctness. Aristotle initially solved a slightly weaker variant but was able to autonomously repair its proof to achieve the full result without human intervention.
Important Caveats
AcerFur emphasized three critical caveats to the achievement. First, the original problem statement is ambiguous, and the model solved an interpretation that the mathematical community deemed as the likely intended meaning to yield non-trivial solutions. Second, the solution appears heavily inspired by previous work by mathematician Carl Pomerance, raising questions about how novel the AI’s contribution truly is. Third, it remains unclear how much currently unfound literature exists on solving special cases of this type of problem.
The solution emerged from a collaborative process between AcerFur and X user Liam06972452, who first received GPT-5.2’s response and requested verification. AcerFur clarified that GPT-5.2 performed the heavy mathematical lifting, while GPT-5.2 Pro was subsequently used to format the proof into a complete LaTeX paper format, possibly validating and filling in gaps during the formatting process.
Building Momentum in AI Mathematics
This achievement comes on the heels of another recent claim by Harmonic, the mathematical AI startup founded by Robinhood CEO Vlad Tenev. In November last year, Harmonic announced that its Aristotle system had solved Erdős Problem #124, which had remained open for nearly 30 years since its publication in a 1995 paper.
However, that claim was met with measured responses from the mathematical community. Thomas Bloom, who maintains the Erdős problems website, acknowledged the achievement as impressive but noted that the solved version was the easier of two variants posed by Erdős, and that the solution turned out to be relatively straightforward in hindsight, comparable in difficulty to mathematical competition problems where AI has already demonstrated strong performance.
Erdős problems refer to mathematical conjectures posed by Paul Erdős, one of the most prolific mathematicians of the 20th century who published over 1,500 papers during his lifetime. Solving an Erdős problem is considered a significant achievement in the mathematical community, with Erdős himself offering monetary prizes for solutions based on his assessment of their difficulty.
The Formal Verification Advantage
Both achievements highlight the importance of formal verification in validating AI-generated mathematical work. Harmonic’s approach centers on using Lean, a formal language that allows every solution to be verified down to foundational axioms, eliminating the need for human mathematicians to manually check the accuracy of outputs.
Earlier in 2025, Harmonic announced that Aristotle achieved Gold Medal-level performance at the 2025 International Mathematical Olympiad, generating verifiably correct solutions to five of six problems. This positioned Harmonic alongside tech giants like Google DeepMind and OpenAI, both of which reported similar results with their respective models.
Implications and Questions
If these claims are validated by the broader mathematical community, they could represent a turning point where AI systems begin contributing original mathematical discoveries rather than simply mastering existing problem sets. However, several questions remain about the true novelty of these solutions, the extent to which they may have been influenced by training data, and whether they represent genuine mathematical insight or sophisticated pattern matching.
The ambiguity around problem #728’s original statement and the acknowledgment that GPT-5.2’s solution builds heavily on prior work underscore the complexity of evaluating AI contributions to mathematics. Even as these systems demonstrate impressive capabilities, the question of whether they are truly conducting novel research or recombining existing knowledge in new ways remains open for debate. What is clear is that AI systems are rapidly approaching, and may have already reached, the threshold of making meaningful contributions to mathematical research. Whether this represents a new era of AI-human collaboration in mathematics — or something even more transformative — remains to be seen.