AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

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

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 Odd Characteristic?

Model / AI: OpenAI (unreleased)

machine-checked (counterexample)self-reported (counterexample)
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 Odd Characteristic'. We construct a counterexample to Kaplansky's direct-finiteness conjecture in odd characteristic. For one specified odd prime p, we obtain a field K of order p4, a finitely generated group G containing torsion, and finite sums a,b\in K[G] with ab=1 but ba\ne1. The same elements define a cellular automaton on KG that is injective but not surjective.

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