Chinese AI Cracks Decade-Old Maths Problem Without Human Intervention

In a significant development for mathematics and artificial intelligence, a Chinese research team has claimed that its AI system has independently solved a long-standing mathematical problem, marking a new step in automated research. According to a team led by Peking University, the artificial intelligence framework resolved an open problem first proposed in 2014 by American mathematician Dan Anderson, reported the South China Morning Post.

The researchers shared their findings in a preprint paper published on April 4, noting that the system worked autonomously to reach the solution. The team said the AI framework analysed decades of mathematical research and connected natural language reasoning with formal machine verification to solve the conjecture. The researchers stated that they successfully solved an open problem in commutative algebra and automatically formalised the proof with essentially no human intervention.

They further said that the system was able to carry out mathematical tasks faster than human mathematicians, including work that usually requires collaboration among experts from different fields.

According to SCMP, the paper noted that this work provides a concrete example of how mathematical research can be substantially automated using AI.

The research, which has not yet been peer-reviewed, was led by Professor Dong Bin. It included experts in both mathematics and artificial intelligence.

The team also included scientists from Westlake University, Tianjin University, and iQuest Research.

According to the researchers, recent advances in large language models (LLMs) have enabled AI systems to move beyond simple problems and solve research-level mathematical challenges. They cited systems like Gemini Deep Think, which achieved gold-medal performance at the 2025 International Mathematical Olympiad.

However, they also clarified that solving complex mathematical problems through AI still often relies on human oversight. They argue that absolute accuracy is essential in mathematical proofs, and even proofs prepared by experts can contain minor errors, while proofs created by AI can be less reliable due to errors.

With this in mind, the team proposed a framework based on two AI agents. The first is an informal reasoning agent named Rethlas, which explores strategies and generates possible proofs using a theorem search engine. The second is a formal verification agent named Archon, which transforms these informal proofs into fully verifiable forms using tools like Lean 4 and its Mathlib library.

This AI framework was applied to Anderson's problem, which involves quasi-complete Noetherian local rings and commutative algebras. After generating an informal proof that disproved the initial assumption, the system completed formal verification within 80 hours.

The researchers stated that the human role was limited to downloading restricted files that the system could not access on its own, and no mathematical judgments were required.

They added that although the AI could solve the problem on its own, guidance from a mathematician could speed up the process. In the end, the team concluded that their results show that informal reasoning agents and formal verification systems together can effectively solve real open problems in mathematics.