A Chinese artificial intelligence system has autonomously solved a decade-old mathematical problem, according to a new study. The algebra conjecture was first posed in 2014 by American mathematician Dan Anderson, a former University of Iowa professor who died in 2022.
The AI, developed by a team at Peking University, processed decades of mathematical literature to crack Anderson's problem and verify its own findings without any human intervention. The researchers described their work in a yet-to-be-peer-reviewed study posted on the arXiv repository.
The system, called Rethlas, draws from a maths theorem search engine named Matlas to explore strategies for solving a problem, following a workflow similar to that used by mathematicians. When Rethlas produces a potential proof, a second system called Archon uses another search engine, LeanSearch, to transform the proof into a project for the interactive theorem prover Lean 4.
Using this framework, the AI solved Anderson's algebra conjecture within 80 hours of runtime. “No mathematical judgement was required from the human operator,” the researchers wrote. However, they noted that the process could be sped up if a mathematician guided Archon.
The study demonstrates how mathematical research can be substantially automated using AI, the team said. While AI systems are being trained worldwide to solve mathematical problems, they typically require significant human supervision. The Chinese scientists emphasised that their approach integrates a natural language reasoning agent with a formalisation agent to ensure rigour and reduce human effort.
