A Torsion-Free Group Algebra That Is Not Directly Finite

Follow-up works

• Seth Douglas, Nidhal Mghirbi, hyperbolic-group-not-sofic (note and Lean formalization) (GitHub, v1.1.0, October 2026). This note on a different OpenAI group (A torsion-free hyperbolic group that is not residually finite) remarks in its introduction that OpenAI's characteristic-two torsion-free groups "with a group algebra that is not directly finite" already show that Linnell division rings need not exist.

Comments and discussion

• Johan Öinert, comment on 100+ reactions to 100+ solutions (proofsandprompts.com, post of 2026-10-08). Öinert observes that the claimed torsion-free example over $\mathbb F_2$ also gives a nontrivial idempotent $ba$, hence a characteristic-two counterexample to the idempotent conjecture, and criticizes the manuscript for not mentioning this.

Formalization

• OpenAI, Lean scope note for family 197 (lean/docs/197.md) (openai/math release, 2026-10-06). The family's scope note covers the characteristic-two, odd-characteristic and determinant companions; it does not list this torsion-free manuscript among the formalized papers. [family-level]

Possibly relevant literature (found by the agent, not checked)

• Francesco Fournier-Facio, A torsion-free non-sofic group (arXiv:2608.02025, August 2026). Gives torsion-free nonsofic groups by a different route; relevant to the manuscript's remark that its torsion-free finitely presented $G$ is nonsofic by Elek–Szabó.
• OpenAI, Ten Advances in Mathematics and Theoretical Computer Science, Chapter 3 "Nonsofic groups exist" (OpenAI, updated 2026-08-06). An earlier claimed explicit nonsofic group (built from the binary Leavitt algebra and Thompson's group $V$), relevant to the nonsoficity consequence stated after Theorem 1.1.
• Michal Doucha, Jakub Gismatullin, On dual surjunctivity and applications (arXiv:2008.10565, 2020). Proves that dual surjunctive groups satisfy direct finiteness over all fields of positive characteristic, so Theorem 1.1 would also imply that $G$ is not dual surjunctive.
• Brandon Seward, Krieger’s finite generator theorem for actions of countable groups II (arXiv:1501.03367, 2015; revised 2019). Its conditional implication from positive Rokhlin entropy for free ergodic actions of every countable group to surjunctivity and direct finiteness provides context for this paper’s claimed counterexample. [family-level]

Digests and expositions

• Ying Xie, What the Machine Invented: Mining New Mathematical Instruments from OpenAI's October 2026 Release of AI-Generated Mathematics (arXiv:2610.17090, 2026-10-12). The card for family 197 (Section 8.4.2) mainly covers the characteristic-two construction and notes as a caveat that this torsion-free companion is not formalized; per the paper, the first extraction for each family used AI readings. [family-level]
• AI Proved What?, One-sided inverse? Kaplansky’s direct-finiteness conjecture (Episode 197, October 2026). This illustrated exposition compares all four papers, explains their construction ideas, and distinguishes their claims and formalization scope. [AI-generated per source] [family-level]

News and blogs

• Kingy.ai, OpenAI's 722 Math Manuscripts: The Results, Proofs, Compute and Costs (October 2026). Notes that the family headline claims the torsion-free strengthening while the Lean scope page covers constructions with torsion, and says the title alone does not show that the torsion-free result was checked. [family-level]