In a significant leap for artificial intelligence, a research team from Peking University has developed an AI system capable of solving complex, unsolved mathematical problems entirely on its own. The system successfully tackled a decade-old algebra conjecture, marking a shift from AI as a mere assistant to AI as an autonomous researcher.
Breaking the Algebra Conjecture
The problem at the center of this breakthrough was an algebra conjecture first proposed in 2014 by the late Dan Anderson, a former professor at the University of Iowa. For ten years, the problem remained an open challenge in the field of commutative algebra.
Unlike previous AI models that require constant human guidance, this new system processed decades of mathematical literature to solve the conjecture and—crucially—verified its own findings without human intervention. The entire process was completed within 80 hours of runtime.
The Architecture of Autonomy: Rethlas and Archon
To overcome the traditional limitations of AI in mathematics, the researchers moved away from standard Large Language Models (LLMs), which are often prone to “hallucinations” or logical errors. Instead, they built a dual-agent framework designed to mimic the rigorous workflow of human mathematicians:
- The Reasoning Agent (Rethlas): This system acts as the “thinker.” It utilizes a theorem search engine called Matlas to explore various strategies and mathematical paths to solve a problem.
- The Formalization Agent (Archon): Once a potential proof is found, Archon takes over. Using LeanSearch, it translates the informal reasoning into a formal, machine-verifiable format.
- The Verifier (Lean 4): The system uses Lean 4, a specialized programming language and interactive theorem prover, to ensure the proof is mathematically sound and free of errors.
Why This Matters: From Assistance to Automation
Current AI trends show a massive push toward training models in mathematics, but most still struggle with the “rigor gap.” While humans can write proofs, they can make mistakes; while LLMs can generate text quickly, they often lack the logical precision required for high-level mathematics.
This Peking University study addresses this gap by integrating natural language reasoning with formal verification. This dual approach ensures that the AI doesn’t just “guess” an answer, but constructs a proof that can be mathematically proven to be correct.
Furthermore, the researchers noted that the AI demonstrated a unique ability to perform tasks that typically require interdisciplinary collaboration, effectively acting as multiple experts working in tandem.
The Future of Mathematical Research
While the system operated autonomously, the researchers noted that human intervention can still act as an accelerator. A mathematician guiding the “Archon” agent can speed up the formalization process, suggesting a future where humans and AI work in a high-speed, symbiotic loop.
“This work provides a concrete example of how mathematical research can be substantially automated using AI,” the researchers stated.
Conclusion
By combining reasoning with rigorous formal verification, this new framework moves AI beyond simple computation and into the realm of autonomous scientific discovery. This breakthrough paves the way for AI to tackle increasingly complex problems in mathematics and other highly technical scientific fields.
