Kaplansky's direct-finiteness conjecture

Kaplansky's direct-finiteness conjecture asks whether, for every field K and every group G, elements a and b of the group algebra K[G] with ab = 1 must also satisfy ba = 1. Four manuscripts dated 23 September to 4 October 2026 in OpenAI's public mathematics collection (github.com/openai/math) claim counterexamples in characteristic two and in odd characteristic, including one over the field with two elements for a finitely presented torsion-free group. As consequences they claim counterexamples to Gottschalk's surjunctivity conjecture for cellular automata and to the group-ring Determinant Conjecture, and finitely presented groups that are not sofic. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

As recounted in the introductions of the manuscripts:
- For finite groups, K[G] is finite dimensional and direct finiteness is elementary. In characteristic zero, Kaplansky's operator-algebra argument proves it for every group, and Montgomery (1969) gave a proof with the identity-coefficient trace that also covers matrix rings (stable finiteness).
- In positive characteristic, Ara, O'Meara and Perera (2002) proved stable finiteness over division rings for free-by-amenable groups, and Elek and Szabó (2004) for all sofic groups. Dykema and Juschenko (2015) showed that stable finiteness is equivalent to direct finiteness after taking products with finite groups. Dykema, Heister and Juschenko proved direct finiteness for several small support pairs over F₂.
- A group is surjunctive if every injective cellular automaton over a finite alphabet on its configuration space is surjective; Gottschalk (1973) conjectured that every group is surjunctive. Gromov and Weiss proved this for sofic groups, and Elek and Szabó recorded that surjunctivity implies direct finiteness over finite fields. Ceccherini-Silberstein, Coornaert and Phung developed the linear and algebraic theory.
- The Determinant Conjecture from the theory of L²-invariants (Lück, Conjecture 13.2) asserts that the Fuglede–Kadison determinant of a matrix over the integral group ring is at least 1. Schick proved it for amenable groups and Elek and Szabó (2005) for sofic groups. The determinant manuscript distinguishes this lower bound from the determinant approximation question, for which Kammeyer gave a counterexample (arXiv:2609.15567).
- Since direct finiteness, surjunctivity and the determinant bound all hold for sofic groups, a counterexample to any of them yields a group that is not sofic. Whether every group is sofic was an open problem.

The original results

Characteristic two (23 September 2026). Theorem 1.1 of the manuscript states that there are a finite field K of characteristic two, a finitely presented group G containing an element of odd prime order, and a, b in K[G] with ab = 1 and ba ≠ 1. The data are specified by a terminating finite prescription, which the manuscript says has not been executed, and K is not asserted to be F₂. By the theorem of Elek and Szabó the group is not sofic, and the same elements give an injective cellular automaton on K^G that is not surjective, so G is not surjunctive.
- Method, as described: finite incidence data from affine lines over a finite field, with a set of points removed and a regular line system of large girth retained by a probabilistic argument, are turned into a matrix pair over a group algebra. Copies of F_ℓ² glued along an incidence structure embed by a planar balance argument, and the matrix obstruction is converted into scalar elements following Dykema and Juschenko. The only imported existence theorem is a uniform bound from Linnik's theorem.
- Source: the manuscript A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Characteristic Two.
The Determinant Conjecture (23 September 2026). Theorem 1.1 of the manuscript states that there are a finitely generated group G_D and a square matrix over Z[G_D], invertible over Q[G_D], whose Fuglede–Kadison determinant lies strictly between 0 and 1. Its existence input is the characteristic-two counterexample above. Source: the manuscript A Counterexample to the Group-Ring Determinant Conjecture.
Odd characteristic (26 September 2026). The manuscript states a counterexample for one specified odd prime p, with a field of order p⁴ and a finitely generated group with torsion, together with the same cellular-automaton consequence. The repository's scope note specifies p as the smallest prime divisor of ((1200 choose 600)!)² + 1. Source: the manuscript A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Odd Characteristic.
Torsion-free, over the field with two elements (4 October 2026). Theorem 1.1 of the manuscript states that there are a finitely presented torsion-free group G, with a finite two-dimensional classifying complex, and a, b, c in F₂[G] with ab = 1, ac = 0 and c ≠ 0, so that ba ≠ 1. By the theorem of Elek and Szabó the group is not sofic. The manuscript describes its method as an adaptation of the graph and cone construction of the collection's torsion-free zero-divisor manuscript (see Kaplansky's zero-divisor conjecture). Source: the manuscript A Torsion-Free Group Algebra That Is Not Directly Finite.
Formalization, as described by the repository. The scope note lean/docs/197.md covers the characteristic-two, determinant and odd-characteristic manuscripts. It lists four Comparator statements: KaplanskyFinitelyPresented.lean, KaplanskyDirectFiniteness.lean, GroupRingDeterminant.lean and OddKaplansky.lean. It states that the nonsofic conclusion is outside these statements and that the determinant manuscript's spectral-measure integral conclusion is not included. The torsion-free manuscript is not listed in the scope note.
Catalogue status. Google DeepMind's Formal Conjectures project still tags gottschalk_surjunctivity_conjecture as research open in FormalConjectures/Wikipedia/SurjunctiveGroup.lean (checked 18 October 2026, at commit 197f7f8); an issue and an open pull request propose to change this (see below).

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 18 October 2026)
2026-10-07	Formal Conjectures issue #6919 by mo271	Statement; status tracking	Reports that the repository's `gottschalk_surjunctivity_conjecture`, tagged research open, appears to be settled by the characteristic-two and odd-characteristic manuscripts. It notes that the release's Lean proofs cover the ring-theoretic statement and, in odd characteristic, injectivity and non-surjectivity of the automaton as a plain map, while continuity and shift-equivariance are not part of the checked statements. A comment by KevorkianPhilippe gives the short bridge for those two properties.	Open issue.
2026-10-08	MathVet (GitHub, review of openai/math, tables at repository commit `c76f1e4`, 14 October 2026)	Review (fidelity of the formal statements)	Rates the family "partial" and records sandboxed Comparator passes for all four challenges. Its note says that the determinant counterexample is stated in Lean and that a Gottschalk counterexample is stated only in odd characteristic, while the characteristic-two statements give a finitely generated or finitely presented group with an element of odd prime order; nonsoficity and the torsion-free claim are not stated.	MathVet states that its ratings concern whether the Lean states the headline claims.
2026-10-08	atimics/math2, Cross-family corollaries of openai/math, entries GR-1, GR-2, GR-10 and GR-11 (GitHub, commit `2c0f005`)	Use (conditional corollaries)	Taking the collection's statements as premises, the catalogue derives that the characteristic-two counterexample survives every field map and that stable finiteness fails over every field of characteristic two (GR-1, in Lean), and that the torsion-free counterexample gives an idempotent ba other than 0 and 1 in F₂[G], so that Kaplansky's idempotent conjecture fails for torsion-free groups in characteristic two (GR-2, a derivation). GR-11 proves in Lean the cellular-automaton consequence for the odd-characteristic statement. GR-10 is a lead on the Aldous–Lyons conjecture.	The catalogue labels each entry by its form of support and states that the entries are conditional on OpenAI's claims.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit `fd4aeeb`, the journal's table of exceptions lists none of the four challenges of this family, so all four were accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-16	J. Jardine, Lattice24, referee review of the torsion-free manuscript in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995)	Review (AI-assisted audit)	The referee review reports no gap after reading every section and recomputing the decay-matrix bounds numerically. Its one minor note is a caution: the claim implies the existence of a non-sofic group, a major open problem, and its correctness rests on a probabilistic exclusion of spherical arrangements with very small margins, whose uniformity claims are only sketched and "deserve an expert's line-by-line check".	Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0.
2026-10-18	Formal Conjectures pull request #7440 by KevorkianPhilippe	Statement; formal link	Restates `gottschalk_surjunctivity_conjecture` as false, adds a counterexample statement, marks both research solved and links the collection's Lean theorem `OAI.OddKaplansky.main_theorem` as the formal proof. The description notes that the link differs from the repository statement by the continuity and shift-equivariance bridge, which is not in the linked proof, and that the preprints' proofs were not read. It states that Claude Code drafted the change under the author's review.	Open pull request, not merged.

Notes

The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.