Research team led by Peking University says dual-agent approach bridges the gap between reasoning and formal machine verification
3-MIN READ3-MIN ListenVictoria BelaPublished: 12:00pm, 13 Apr 2026A Chinese artificial intelligence framework has autonomously resolved an open problem proposed more than a decade ago by a US mathematician, according to the Peking University-led team that developed it.The dual-agent framework solved the problem posed in 2014 by former University of Iowa professor Dan Anderson – who died in 2022 at the age of 73 – the researchers said in a preprint paper published on April 4.By synthesising decades of mathematical literature, the Chinese team’s AI framework bridged the gap between natural language reasoning and formal machine verification to resolve Anderson’s conjecture and verify its own findings, they said.
“Using this framework, we successfully solved an open problem in commutative algebra and automatically formalised the proof with essentially no human intervention,” the researchers wrote in the paper, published in the open-access online research repository arXiv.
The team’s AI framework was able to perform mathematical tasks faster than human mathematicians, including independently doing work that would typically require collaboration between experts in different fields.
China’s latest tech craze is chasing ‘lobsters’ with AI agent OpenClaw
China’s latest tech craze is chasing ‘lobsters’ with AI agent OpenClaw“This work provides a concrete example of how mathematical research can be substantially automated using AI,” according to the paper, which has not yet been peer reviewed.
