A counterexample to Kaplansky's quasitrace conjecture and failure of tensor-product stable finiteness

Lean formalization in OpenAI math repository (Result 294)

Model / AI: OpenAI (unreleased)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'A counterexample to Kaplansky's quasitrace conjecture and failure of tensor-product stable finiteness'. We refute Kaplansky's quasitrace conjecture by constructing a separable unital complex C∗-algebra that admits normalized 2-quasitraces but has no tracial state. As a consequence, we show that the minimal tensor product of two unital simple stably finite complex C∗-algebras can be properly infinite, even when one factor is the reduced free-group algebra C_r^*(\mathbb F_2).

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

• Paper — Paper
• Lean — Lean formalization note
• Code — OpenAI math repository