Chinese AI Achieves Breakthrough by Solving Decade-Old Math Problem
A Chinese artificial intelligence system has autonomously solved a decade-old algebra conjecture, originally proposed by an American mathematician, according to a new study. This breakthrough highlights the potential for automating mathematical research with minimal human intervention.
Details of the AI System and Its Achievement
The algebra conjecture was first posed in 2014 by Dan Anderson, a former University of Iowa professor who passed away in 2022. An AI system 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 oversight.
Using this framework, the researchers stated in a yet-to-be peer-reviewed study posted on the arXiv repository, "we successfully solved an open problem in commutative algebra and automatically formalised the proof with essentially no human intervention."
Scientists observed that the AI system could perform mathematical tasks faster than any human, including independently handling work that typically requires collaboration between experts from different fields.
How the AI System Operates
The new AI applies a reasoning system called Rethlas, which draws from the maths theorem search engine, Matlas, to explore strategies for solving problems, following a workflow similar to that used by mathematicians. When Rethlas generates a potential proof, a second system called Archon uses another search engine, LeanSearch, to transform the proof into a project for an interactive theorem prover.
This theorem prover, Lean 4, is also a programming language with a community-maintained library containing hundreds of thousands of theorems and definitions. Researchers used the AI system to solve Anderson's algebra conjecture within 80 hours of runtime.
Implications for Mathematical Research
"This work provides a concrete example of how mathematical research can be substantially automated using AI," said the researchers, led by Peking University mathematician Dong Bin. They noted that while AI systems globally are trained to solve mathematical problems, they often require significant human supervision due to the rigour needed in proofs.
Mathematical proofs demand complete rigour, yet even expert-written proofs may contain subtle flaws, and proofs produced by large language models (LLMs) are prone to hallucination and less reliable. "Motivated by this, we propose a framework for autonomously tackling and verifying research-level mathematics that integrates a natural language reasoning agent with a formalisation agent," the Chinese scientists wrote.
Researchers found they could speed up the process if a mathematician guided Archon, but the system operated independently. "No mathematical judgment was required from the human operator," they wrote.
Future Prospects and Conclusions
"Our work illustrates a promising paradigm for mathematical research in which informal and formal reasoning systems, equipped with theorem retrieval tools, operate in tandem to produce verifiable results, and substantially reduce human effort," the team noted. This advancement could revolutionise how complex mathematical problems are approached, paving the way for more efficient and automated research methodologies in the future.
