A research team from Peking University has achieved a milestone by using artificial intelligence to solve an open problem in commutative algebra for the first time in China, as announced in April 2026. Known as the Anderson conjecture, the problem had remained unresolved for over a decade since it was first proposed in 2014 by American mathematician D.D. Anderson. The team, named AI4Math and led by Professor Dong Bin from the Beijing International Center for Mathematical Research at Peking University, developed an automated AI framework to tackle the challenge and completed a large-scale formal verification of the solution.
The Anderson conjecture concerns the properties of “quasi-complete local rings”, algebraic structures that describe infinitesimal features and deformations of geometric objects at a local scale. Despite efforts from the mathematical community, no human proof had been found since the conjecture was proposed. In their approach, the AI4Math team designed a dual-agent collaboration system. One agent, Rethlas, retrieved relevant mathematical statements from millions of entries, while the other agent, Archon, translated the reasoning into formal code using Lean, a programming language and theorem prover. During the process, Archon autonomously identified hidden logical flaws in the initial approach and redesigned the overall proof strategy.
This breakthrough was supported by years of foundational work. The AI4Math team, formally established in 2023, brought together researchers from algebra, number theory, optimization, machine learning, and artificial intelligence. Central to their effort was a dual-engine retrieval architecture that includes LeanSearch and Matlas. LeanSearch allows semantic retrieval of relevant theorems using natural language queries and has since been widely adopted by the Lean community. Matlas covers tens of millions of mathematical statements and supports proposition-level retrieval. These tools enabled the AI to locate a seemingly unrelated theorem about integral closure completions, which was then used to construct a counterexample that resolved the conjecture.
Academic leaders have praised the achievement for opening new pathways in the integration of mathematics and AI. Liu Ruochuan, Dean of the School of Mathematical Sciences at Peking University and an academician of the Chinese Academy of Sciences, noted that the exploration not only solved a concrete mathematical problem but also validated a new research paradigm at the intersection of AI and mathematics. Tian Gang, also an academician of the Chinese Academy of Sciences, called for continued support for young researchers to pursue bold innovation in this direction. As the first instance in China of an AI framework solving an open problem in commutative algebra, announced in April 2026, this work demonstrates the potential of artificial intelligence to contribute to fundamental mathematical research.