Recently, the mathematics community has witnessed a milestone breakthrough in artificial intelligence. Neel Somani, a former quant researcher, discovered that AI provided a complete proof for an unsolved problem of the mathematical legend Paul Erdős within just 15 minutes of thinking, and its rigor has been verified by formal tools such as Lean.
For a long time, the more than 1,000 mathematical conjectures left by Erdős were seen as the boundary of human intelligence. However, since last Christmas, 15 problems on this site have been marked as "solved," among which 11 solutions clearly involved AI.
Somani pointed out that GPT5.2 demonstrated an unprecedented level of proficiency in mathematical reasoning. It not only skillfully applied axioms such as Legendre's formula but also provided a more complete solution based on previous research by Harvard mathematician Noam Elkies. This mass solving of "long-tail" mathematical problems has sparked a wide discussion on whether LLMs are expanding the boundaries of human knowledge.
Fields Medalist Terry Tao made a detailed statistical analysis of this development on his GitHub page, documenting eight cases where AI achieved autonomous progress. He speculated that AI's scalability gives it an advantage over humans in handling obscure and simple "long-tail" problems.
Aside from the evolution of the model itself, the involvement of formal tools (such as Aristotle from Harmonic) is also crucial. These tools can automatically convert AI-generated reasoning into computer-verifiable code, greatly simplifying the verification process. Tudor Achim, founder of Harmonic, said that compared to the number of problems solved, the fact that world-class mathematics professors are publicly admitting to using AI tools is the most convincing evidence of AI's capabilities.
