Kaplansky’s zero-divisor and direct-finiteness conjectures refuted? (OpenAI, Lean)

Your AI and this story

Key facts

• Zero divisors (family 196): Theorem 1.1, ‘There exist a finitely presented torsion-free group G and nonzero elements α, β ∈ F₂[G] such that αβ = 0. Moreover, G admits a finite two-dimensional classifying space.’ The paper traces the question to Higman’s 1940 thesis and Kaplansky’s 1956 problem list, and contrasts it with Gardam’s 2021 refutation of the related unit conjecture (‘a nontrivial unit is not a zero divisor’). Lean challenge TorsionFreeZeroDivisors: ‘accepted’ (oai-math-revised comparator run, 25–26 Oct)
• Direct finiteness (family 197, four manuscripts): characteristic two, 23 Sept, 28 pages (‘We disprove Kaplansky’s direct-finiteness conjecture by constructing a finite field K of characteristic two, a finitely presented group G, and finite sums a,b ∈ K[G] with ab=1 but ba≠1. The group G is nonsofic. The same elements define a cellular automaton on K^G that is injective but not surjective, disproving Gottschalk’s surjunctivity conjecture’); odd characteristic, 26 Sept, 25 pages (a field of order p⁴ for one specified odd prime p); torsion-free over F₂, 4 Oct, 31 pages (‘a finitely presented torsion-free counterexample to Kaplansky’s direct finiteness conjecture over the field of two elements’)
• Why non-sofic groups are needed (papers’ history sections): Elek and Szabó (2004) proved stable finiteness of K[G] for all sofic G, and Gromov and Weiss proved sofic groups surjunctive, so any counterexample group is non-sofic. In characteristic zero group algebras are always directly finite (Kaplansky). OpenAI’s Astra had claimed the first non-sofic group in August 2026 (see OpenAI’s unreleased ‘Astra’ model claims ten advances in maths and theoretical CS, with Lean proofs)
• Determinant Conjecture (23 Sept, 9 pages): ‘We construct a finitely generated group G and a square matrix over Z[G] that is invertible over Q[G] and has Fuglede–Kadison determinant strictly between zero and one’, refuting the unrestricted group-ring Determinant Conjecture
• Lean scope (lean/docs/197.md): the characteristic-two statements use a group with an element of odd prime order, and ‘The further conclusion that the group is nonsofic is outside these statements’; the odd-characteristic statement uses a field of order p⁴, with p the smallest prime divisor of ((1200 choose 600)!)² + 1. Carlos Toledo’s audit (finding G2) notes that the family headline is the torsion-free example while ‘the finitely presented Lean statement REQUIRES the group to contain an element of odd prime order’, and that the Kaplansky witnesses are prescriptions with no explicit instance published
• Reactions (Proofs and Prompts, 8 Oct): Michael Chapman listed ‘the refutations to the Kaplansky conjectures’ among problems ‘I grew up on’. Johan Öinert observed that the torsion-free F₂ example gives ba as a nontrivial idempotent, hence a characteristic-2 counterexample to the idempotent conjecture: ‘Yet, there is no mentioning of this obvious conclusion in the latter document! … This is NOT how human mathematicians write papers!’ Formal Conjectures (Google DeepMind) restates the zero-divisor conjecture as false citing the paper, and merged PR #7440 (19 Oct) restating Gottschalk’s conjecture as false
• Converse claim (family 207, 24 Sept): ‘for every torsion-free group G and every commutative unital domain R of characteristic zero, the only idempotents in RG are 0 and 1. This proves Kaplansky’s idempotent conjecture in characteristic zero’, via the Bass trace conjecture (Lean: BassTrace, BassTorsionFree accepted). Indira Chatterji, who proved the amenable case with Berrick and Mislin: ‘I don’t understand the proof, and I still don’t believe that this conjecture could be true in general.’ Roman Sauer recognised a trick from his own work in OpenAI’s ‘deeply creative solutions of problems 207 and 335’