Chinese AI Solves Open Mathematical Problem, Verifies Proof

By synthesising decades of mathematical literature, a Chinese team’s AI framework has bridged the gap between natural language reasoning and formal machine verification to resolve Anderson’s conjecture and verify its own findings.

“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.

“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.