Papers With

← All papers
First page of On some open problems in commutative algebra resolved by Rethlas

On some open problems in commutative algebra resolved by Rethlas

Jiedong Jiang, Yixiao Li, Zeming Sun, Yuefeng Wang, Liang Xiao, Jiahong Yu

math.AC May 24, 2026 · v2
autoformalization formalization algebra
Read PDF arXiv abstract Code
TL;DR
The counterexample to Anderson's quasi-completeness conjecture was auto-formalized and machine-checked in Lean 4 by the Archon system.
Abstract
We report on a collection of open problems in commutative algebra and related areas that have been resolved (proved or disproved) using the Rethlas natural-language automated reasoning system. The problems are drawn from several published lists, including Open Problems in Commutative Ring Theory (Cahen-Fontana-Frisch-Glaz), Erman-Sam's survey of Boij-Söderberg theory. For each problem we record the precise statement and a self-contained proof produced (with no human intervention) by Rethlas and subsequently verified by human experts.
Problem

Several open problems in commutative algebra remained unresolved. They come from the volume Open Problems in Commutative Ring Theory and from a survey of Boij–Söderberg theory, and concern GCD-like conditions on group rings, quasi-completeness, and biring structures on integer-valued polynomial rings.

Approach

The Rethlas natural-language automated reasoning system produced self-contained proofs or counterexamples with no human intervention. Human experts then verified the proofs. One result, a weakly quasi-complete Noetherian local ring that is not quasi-complete, was then auto-formalized in Lean 4 by the Archon system.

Results

Finite conductor and quasi-coherent properties do not ascend from G-GCD rings to group rings. Certain AGCD domains are shown to have finite t-character. Anderson's conjecture is resolved negatively, with a Lean 4 machine-checked proof. Int(D) need not admit a compatible biring structure.