A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Characteristic Two

Does the classical conjecture or property hold, or does there exist a counterexample as established in A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Characteristic Two?

Oct 6, 2026

Lean formalization in OpenAI math repository (Result 197)

Model / AI: OpenAI (unreleased)

machine-checked (counterexample)self-reported (counterexample)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'A Counterexample to Kaplansky's Direct-Finiteness Conjecture in Characteristic Two'. 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\in K[G] with ab=1 but ba\ne1. The group G is nonsofic. The same elements define a cellular automaton on KG that is injective but not surjective, disproving Gottschalk's surjunctivity conjecture.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 197). The Lean development was not rebuilt locally.