A Chinese AI framework autonomously solved an open problem from 2014 in commutative algebra, proposed by US mathematician Dan Anderson, marking a milestone in automated mathematical reasoning and verification.

The project was led by Peking University with collaborators from Westlake University, Tianjin University, and IQuest Research, and the findings are documented in an arXiv preprint not yet peer-reviewed.

The system uses a dual-agent setup that pairs a natural language reasoning agent (Rethlas) with a formal verification agent (Archon) to generate and verify proofs, translating informal reasoning into Lean 4 formal proofs via LeanSearch and the Mathlib library.

Experts emphasize integrating informal reasoning with formal verification to push autonomous progress in genuine open problems, while noting AI proofs require careful human-verified checks due to possible errors or hallucinations in LLM-driven steps.

The framework completed formalisation within about 80 hours of agent runtime, with human work limited to downloading paywalled sources Archon could not access.

A preprint posted on arXiv on April 4 outlines how the dual-agent AI bridged natural language reasoning and formal machine verification to reach and check the solution.

This result demonstrates substantial automation in mathematical research, showing AI can propose solutions and formalize/validate proofs, though the paper remains not yet peer-reviewed.

The AI system synthesized decades of mathematical literature to complete the problem-solving process, achieving faster-than-human performance across tasks that typically require multi-domain collaboration.

The open problem deals with quasi-complete Noetherian local rings in commutative algebra, with the AI producing a counter-example proof and formalizing it with minimal human input.