Gottschalk Surjunctivity Conjecture

The Gottschalk surjunctivity conjecture asserts that every group is a surjunctive group (Gottschalk 1973).

OpenAI (2026, pp. 1, 23) constructed a counterexample using a finite field with elements for a specified odd prime number and a finitely generated group containing torsion. There are with and , refuting the Kaplansky direct-finiteness conjecture. For , where is the group algebra, define

Only finitely many coefficients are nonzero, while may be any configuration in . The finite dependence makes continuous. For the left shift group action , the identity makes it an equivariant map. The relation and the fact that is the identity map give , so is injective. If has , the configuration that equals 1 at and 0 elsewhere is outside the image of . Indeed, the image consists of fixed points of , whereas . Thus is not surjective, even when preimages of arbitrary support are allowed.

MathVet (2026) published a successful Lean-kernel check of the algebraic construction and the injectivity and failure of surjectivity of , using only Lean's standard axioms. The linked formal theorem does not include continuity and shift equivariance, which follow from the displayed formula with finite support. The published checking run has not been independently repeated here. The theorem does not assert a finitely presented or torsion-free group counterexample.