Chinese AI cracks decade-old maths problem without human oversight

A Chinese artificial intelligence system has solved a decade-old problem proposed by an American mathematician, according to a new study.

The algebra conjecture was first posed in 2014 by then University of Iowa professor Dan Anderson, who died in 2022.

An AI system developed by a Peking University team processed decades of mathematical literature to crack Anderson’s problem and verify its own findings without any human intervention.

“Using this framework,” the team said in a yet-to-be peer-reviewed study posted in the arXiv repository, “we successfully solved an open problem in commutative algebra and automatically formalised the proof with essentially no human intervention.”

Scientists observed that the AI system could perform mathematical tasks faster than any human, including independently doing work that normally required collaboration between different field experts.

“This work provides a concrete example of how mathematical research can be substantially automated using AI,” the researchers, led by Peking University mathematician Dong Bin, said.

AI systems are being trained across the world to solve mathematical problems, but they still require a large amount of human supervision to crack math problems. “Mathematical proofs demand complete rigour, yet even expert-written proofs may contain subtle flaws and proofs produced by LLMs, which are prone to hallucination, are far less reliable,” the Chinese scientists wrote in the latest study.

“Motivated by this, we propose a framework for autonomously tackling and verifying research-level mathematics that integrates a natural language reasoning agent with a formalisation agent.”

The new AI applies a reasoning system called Rethlas, which draws from the maths theorem search engine, or Matlas, to explore strategies for solving a problem, following a workflow similar to what mathematicians use.

When Rethlas comes up with a potential proof, a second system called Archon uses another search engine called LeanSearch to transform the proof into a project for an interactive theorem prover.

This theorem prover, Lean 4, is also a programming language with a community-maintained library that has hundreds of thousands of theorems and definitions.

Researchers used the new AI system to solve Anderson’s algebra conjecture within 80 hours of runtime.

“No mathematical judgment was required from the human operator,” they wrote.

However, researchers found that they could speed up the process if a mathematician guided Archon.

“Our work illustrates a promising paradigm for mathematical research in which informal and formal reasoning systems, equipped with theorem retrieval tools, operate in tandem to produce verifiable results, and substantially reduce human effort,” they noted.