- Dual-agent AI system autonomously solved 2014 Anderson conjecture
- Rethlas explores problem-solving strategies like a human mathematician would
- Archon transforms potential tests into projects for the Lean 4 tester
A research team led by Peking University developed a dual-agent artificial intelligence system capable of solving advanced mathematical problems while verifying its own results.
The system solved a conjecture proposed in 2014 by Dan Anderson, completing the process within 80 hours of execution.
“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 in a preprint paper posted on arXiv.
Article continues below.
How the Dual Agent Framework Really Works
The artificial intelligence tool applies a reasoning system called Rethlas, which relies on a mathematical theorem search engine called Matlas to explore problem-solving strategies.
When Rethlas produces a potential proof, a second system called Archon uses another search engine called LeanSearch to transform that proof into a blueprint for an interactive theorem prover.
The theorem prover, Lean 4, is also a programming language with a community-maintained library containing hundreds of thousands of theorems and definitions.
The researchers observed that no mathematical judgment was required by the human operator during the problem-solving process.
The AI system performed mathematical tasks faster than any human, including independent work that would normally require collaboration between experts in different fields.
However, the team also discovered that a mathematician could speed up the process by guiding Archon when necessary.
“This work provides a concrete example of how mathematical research can be substantially automated using AI,” the researchers said.
Mathematical proofs require complete rigor, but even proofs written by experts can contain subtle flaws.
Similarly, tests produced by large language models are prone to hallucinations and are much less reliable than formal verification methods.
The Chinese team’s framework bridges the gap between natural language reasoning and formal machine verification, allowing the AI system to solve problems and verify its own findings.
“Our work illustrates a promising paradigm for mathematical research in which formal and informal reasoning systems operate together to produce verifiable results,” the researchers noted.
The document has not yet been peer-reviewed, so independent verification is still pending.
Anderson’s conjecture was a relatively obscure problem in commutative algebra, making the AI’s achievement noteworthy.
However, this feat is not comparable to solving a Millennium Prize-level challenge like the Riemann Hypothesis or the P vs NP problem.
It remains to be seen whether this approach scales to more difficult mathematical problems.
That said, for a field that has resisted automation for centuries, this represents a notable milestone.
Through the independent
Follow TechRadar on Google News and add us as a preferred source to receive news, reviews and opinions from our experts in your feeds. Be sure to click the Follow button!
And of course you can also follow TechRadar on TikTok for news, reviews, unboxings in video form and receive regular updates from us on WhatsApp also.
