Anderson’s quasi-completeness problem

Anderson's quasi-completeness problem

Model / AI: Rethlas, Archon

the Rethlas and Archon agents settled Problem 8a of *Open Problems in Commutative Ring Theory* in the negative with essentially no human mathematical input; the 19k-line Lean formalization builds clean and passes a statement-matching check. A follow-up reports human experts verifying eight Rethlas results including this one, though only this one is formalized.

Source review pending. Imported from the original notes; linked claims and artifacts have not been re-audited in this restructuring.

• Paper — Anderson's quasi-completeness problem
• Lean — 19k-line Lean formalization
• Paper — follow-up