Oct 6, 2026
Lean formalization in OpenAI math repository (Result 196)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'A Torsion-Free Group Algebra with Zero Divisors'. We disprove Kaplansky's zero-divisor conjecture by constructing a finitely presented torsion-free group G for which \mathbb F_2[G] has nonzero zero divisors. The group admits a finite two-dimensional classifying space.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 196). The Lean development was not rebuilt locally.