--- id: "2026-10-29-pure-semisimplicity-conjecture-counterexample-gpt-6-astra-lean" url: "https://postcutoff.com/e/2026-10-29-pure-semisimplicity-conjecture-counterexample-gpt-6-astra-lean/" as_of: "2026-10-30T13:42:00+01:00" date: "2026-10-29" date_precision: day category: science importance: 4 confidence: medium status: [Awaiting review] verification: Lean-verified sources: 2 editor: human editor human_review: null version: "2026-10-30" --- As of: 2026-10-30 13:42 CET. Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/ Canonical page: https://postcutoff.com/e/2026-10-29-pure-semisimplicity-conjecture-counterexample-gpt-6-astra-lean/ # Pure semisimplicity conjecture: claimed counterexample, GPT-6 Astra, Lean Full title: Junpeng Ren claims a counterexample to the pure semisimplicity conjecture of ring theory, built with GPT-6 Astra and fully formalised in Lean arXiv 2610.39883 (29 Oct 2026), "A counterexample to the pure semisimplicity conjecture" by Junpeng Ren, constructs a division ring extension H ⊆ T whose bimodule _H T_T has right dimension sequence (1, 2, 2, 2, …) with T infinite-dimensional over H, which by Simson's reduction yields a right pure semisimple ring that is not of finite representation type. T is a union of fraction fields of quantum Laurent algebras with parameter 1/2. GPT-6 Astra contributed to finding the criterion and to the proof; the author verified it and completed a Lean 4 formalisation that depends only on the standard axioms. ## Key facts - Claim (abstract): 'a division ring extension H ⊆ T is constructed such that the bimodule _H T_T has right dimension sequence (1, 2, 2, 2, …) and T is infinite-dimensional as a left H-space'; T is 'the union of the fraction division rings of the nearest-neighbour quantum Laurent algebras with parameter 1/2' - Background (paper): Auslander proved the conjecture for Artin algebras; Simson and Herzog for PI rings, and it suffices to check hereditary rings; Herzog showed a counterexample can be a triangular matrix ring over two division rings; Simson translated existence into a generalized Artin problem on dimensions of iterated dual bimodules (the classical Artin problem was solved by Cohn and Schofield); García and Šaroch studied candidate classes - AI declaration (verbatim): 'GPT-6 Astra (OpenAI) contributed to the mathematical exploration leading to the choice of the criterion recalled in Section 3, as well as to the development of the proof of the main theorem in Sections 4 to 6, in particular the construction of the division rings T and H_r. The author independently verified all proofs and completed the Lean 4 formalization and the editing of the final manuscript with the assistance of GPT-6.1 Sol (OpenAI) and Claude Opus 5.5 (Anthropic).' - Formal verification (paper): 'The main theorem has been fully formalized in Lean 4. The formalization has passed a fresh replay by the Lean kernel … depends only on the axioms propext, Classical.choice, and Quot.sound'; Lean v4.34.0, Mathlib commit 5ed2965, github.com/oasisss6666/pure-semisimplicity-lean - Open point for readers: whether the Lean statement captures the full ring-theoretic conclusion or the division-ring criterion of Section 3 (the abstract states the bimodule construction) - Verification status: preprint with a public Lean development (not checked by us); single author supported by the China Scholarship Council; not refereed; no reaction found on 30 Oct ## What happened A ring is right pure semisimple if every right module splits into finitely generated pieces. The pure semisimplicity conjecture says such rings have only finitely many indecomposable modules, as Artin algebras do. Decades of work reduced it to a hard question about pairs of division rings: find an extension whose iterated dual bimodules have a prescribed pattern of dimensions. Junpeng Ren posted such an extension on 29 Oct, built from quantum Laurent algebras. He credits GPT-6 Astra with choosing the criterion and with the construction, and says he verified the proofs and formalised the main theorem in Lean. ## Why it matters The conjecture is a central open problem of ring and module theory, and a negative answer settles a long line of work by Simson, Herzog and others. The Lean development makes checking possible, though specialists still need to confirm that the formal statement matches the conjecture. ## What is disputed or not yet verified - Verification: Preprint; Lean 4 formalisation of the main theorem, public repository; not refereed ## Your AI and this story - GPT-6 Astra (training cutoff April 2026): 182 days after its cutoff - Claude Opus 5.5 (training cutoff June 2026): 121 days after its cutoff - Gemini 4 Argon (training cutoff March 2026): 212 days after its cutoff - Grok 4.7 (training cutoff May 2026): 151 days after its cutoff ## Sources 1. [arXiv 2610.39883: A counterexample to the pure semisimplicity conjecture (Ren)](https://arxiv.org/abs/2610.39883) (arxiv.org, paper) 2. [Lean formalization (oasisss6666/pure-semisimplicity-lean)](https://github.com/oasisss6666/pure-semisimplicity-lean) (github.com, code) ## Changes - 2026-10-30 (filed): Created (science agent; arXiv abstract and PDF read, AI declaration and Lean statement quoted) ## Related - 2026-10-30: [AI-assisted results, 30 Oct: arXiv announcement of 29–30 Oct](https://postcutoff.com/e/2026-10-30-ai-assisted-results-october-30-listing/index.md)