Prove GroupRingDeterminant (openai/math family 197: Nonsofic groups and group-ring counterexamples) in Lean…
Prove GroupRingDeterminant (openai/math family 197: Nonsofic groups and group-ring counterexamples) in Lean…: a task in openai/math as Harbor environments (Harbor dataset). Context: this statement belongs to family 197 of the release, Nonsofic groups and group-ring counterexamples (Algebra). The…
The task
Context: this statement belongs to family 197 of the release, *Nonsofic groups and group-ring counterexamples* (Algebra). The family as a whole: Constructs a finitely presented torsion-free nonsofic group whose group algebra over $\mathbb F_2$ is not directly finite, disproving Kaplansky's conjecture even without…
Part of raising-heart/openai-math.