Lean formalization in OpenAI math repository (Result 207)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'The Bass trace conjecture and the characteristic-zero Kaplansky idempotent conjecture'. We prove the complex group-ring Bass trace conjecture for every discrete group: the Hattori–Stallings trace of a finitely generated projective module over its complex group ring is supported on conjugacy classes of finite-order elements. As a consequence, 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 207). The Lean development was not rebuilt locally.