Overview
- A Peking University-led team reported in an arXiv preprint that a dual-agent AI solved an open problem in commutative algebra and produced a machine-checked proof.
- The framework pairs a reasoning agent called Rethlas, which searches past papers to draft a proof, with a second agent named Archon that turns the draft into Lean 4 code for formal verification.
- The researchers said the system completed the task in about 80 hours without human judgment, though they noted a mathematician’s guidance made it faster.
- The study has not undergone peer review and independent mathematicians have not yet verified the proof or replicated the workflow.
- The problem was posed in 2014 by University of Iowa mathematician Dan Anderson, and the team argues the approach could ease the heavy work of translating human math into code-checked proofs.