30年数学难题，AI仅6小时告破，陶哲轩：ChatGPT们都失败了

Core Insights - The AI mathematician "Aristotle" developed by HarmonicMath has independently solved the Erdős problem 124, a mathematical challenge that remained unsolved for 30 years, in just 6 hours, marking a significant milestone in the field of mathematics [1][7][9]. Group 1: AI Breakthrough - The AI completed the proof using the Lean proof system, taking only 1 minute for verification, with no human assistance involved [2][15]. - This achievement has been likened to a "moon landing" moment for the mathematics community, indicating a transformative era in mathematical proofs through AI [2][4]. Group 2: Problem Details - The core of Erdős 124 involves determining whether any large number can be represented in binary form under extreme constraints, a question that delves into the depths of combinatorial mathematics [9][11]. - The problem was originally proposed in the paper "Complete sequences of sets of integer powers" and has significant symbolic value in the mathematical community, often seen as a badge of honor for mathematicians [7][9]. Group 3: Community Response - Notable mathematician Terence Tao praised the AI's accomplishment, highlighting the shift in the mathematical landscape towards automation and AI-driven solutions [5][16]. - The success of "Aristotle" contrasts with other AI tools like ChatGPT and Gemini, which failed to provide new insights on the problem [15]. Group 4: Future Implications - The current trend suggests that many unsolved mathematical problems are within reach of AI, particularly those that have been overlooked due to limited human resources [18][20]. - The automation of solving simpler problems could lead to a significant increase in new mathematical results, as AI tools can efficiently tackle issues that have not received adequate attention from human mathematicians [18][20].