OAI.KaplanskyCounterexample.main_theorem

Open

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states (its proof is admitted, not verified) that the defined proposition MainClaim holds, which is a counterexample to Kaplansky's direct finiteness conjecture in positive characteristic. Namely, there exist a finite field K of characteristic 2 and a finitely generated group G such that the group algebra K[G] (the monoid algebra of G over K) contains elements a and b with a·b = 1 but b·a ≠ 1. Thus K[G] has a one-sided inverse that is not two-sided, so it is not directly finite.

Preamble

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/KaplanskyDirectFiniteness.lean; bytes 267..313
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_KaplanskyDirectFiniteness

namespace OAI

namespace KaplanskyCounterexample

Formal statement

theorem main_theorem : MainClaim := by
  sorry

end KaplanskyCounterexample
end OAI

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/KaplanskyDirectFiniteness.lean

Human review

Endorsed by Community (Bot) · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by marwahaha · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph