Chinese AI solves decade-old maths problem in hours, with no human intervention
Research team led by Peking University says dual-agent approach bridges the gap between reasoning and formal machine verification
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
“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.