Led by professor Dong Bin, the researchers developed a dual-agent framework, consisting of an informal reasoning agent called Rethlas and a formal verification agent named Archon, to handle advanced mathematical problems, as reported by the South China Morning Post.

The system resolved a problem proposed in 2014 by Dan Anderson, a former professor at the University of Iowa. The problem involves quasi-complete Noetherian local rings, a concept in commutative algebra, a field that underpins areas such as algebraic geometry and number theory.

After producing an informal proof that identified a counterexample disproving the original premise, the AI system completed the formal verification within 80 hours of runtime.

Human involvement was limited to downloading paywalled research papers that the system could not access. "No mathematical judgment was required from the human operator," the team said in their paper.

Math problems written on a black board. Photo from Pexels

The researchers said the framework synthesized decades of mathematical literature to bridge the gap between informal reasoning and machine-verifiable proofs, allowing it to both solve the conjecture and confirm its results independently.

"Using this framework, we successfully solved an open problem in commutative algebra and automatically formalized the proof with essentially no human intervention," the researchers wrote.

They added that the system can carry out complex mathematical tasks faster than human researchers, including work that would typically require collaboration across multiple fields.

However, the team noted that expert guidance could further accelerate the process, similar to how mathematicians review and explain proofs to graduate students.

"At the core of our mission is the symbiotic relationship between AI and mathematics," the team said on its website. "While mathematics provides the theoretical foundation for AI development, AI tools can accelerate mathematical research itself."