we-solve (beta)

Math-2187-A1 · revision r1 · on Math-2187

OpenAI claim summary for Math-2187

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status at unsolvedmath.com: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

The characteristic-two torsion-free example gives both nonzero zero divisors and a scalar idempotent distinct from zero and one, refuting those two bundled universal assertions. The selected Bass trace papers prove characteristic-zero scalar-idempotent triviality, which is compatible with the positive-characteristic counterexample. The bundle's integral-unit assertion is not settled by these selected results.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Kaplansky's Conjectures
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Manuscript 1.
  5. Manuscript 2.
  6. Manuscript 3.
  7. Manuscript 4.
  8. Outline of the argument
  9. Formal verification
  10. Status caveat
  11. Sources

Kaplansky's Conjectures

OpenAI's claim

The linked manuscripts present the following claims by OpenAI: A finitely presented torsion-free group is claimed to have nonzero elements $a,c\in\mathbb F_2[G]$ with $ac=0$, despite admitting a finite two-dimensional classifying complex; Another construction claims a torsion-free, finitely presented $G$ for which $\mathbb F_2[G]$ contains $a,b$ satisfying $ab=1$ and $ba\ne1$; The Bass trace restriction is claimed for complex group rings of arbitrary discrete groups, implying triviality of scalar idempotents for torsion-free groups over characteristic-zero domains; For every discrete group, the trace of an idempotent matrix over $\ell^1(G;\mathbb C)$ is claimed to vanish outside a finite collection of finite-order conjugacy classes. Together they provide the following support within the scopes described below.

Mathematical statement of the claimed result

Manuscript 1.
For some torsion-free, finitely presented group $G$ admitting a finite two-dimensional classifying space, the source claims \[ \exists\alpha,\beta\in\mathbb F_2[G]\setminus\{0\},\qquad\alpha\beta=0. \] The coefficients are in the field with two elements. This is a zero-divisor example, without a claim here about integral units.
Manuscript 2.
The construction supplies a torsion-free, finitely presented group $G$, with a finite two-dimensional $K(G,1)$, and elements of its characteristic-two group algebra satisfying \[ a,b,c\in\mathbb F_2[G],\qquad ab=1,\quad ac=0,\quad c\ne0,\quad ba\ne1. \] In particular, $a\ne0$ and $e=ba$ obeys $e^2=e$, $e\notin\{0,1\}$. Thus this same example supplies failures of direct finiteness, absence of zero divisors, and triviality of scalar idempotents. These assertions concern $\mathbb F_2[G]$; the separate integral-unit assertion is not a consequence.
Manuscript 3.
For an arbitrary discrete group $G$, let $\operatorname{HS}_G$ be the Hattori--Stallings trace, whose value at a conjugacy class sums the coefficients on that class. For every $x\in K_0(\mathbb C[G])$, \[ |g|=\infty\quad\Longrightarrow\quad\operatorname{HS}_G(x)([g])=0. \] The torsion-free corollary states that, for every $q\ge1$ and idempotent $e\in M_q(\mathbb C[G])$, its identity-coefficient trace equals the rank of its augmentation matrix: \[ \tau_{G,q}(e)=\operatorname{rank}_{\mathbb C}(\epsilon_{G,q}(e)). \] For such $G$, any commutative unital domain $R$ of characteristic zero satisfies \[ e\in R[G],\ e^2=e\quad\Longrightarrow\quad e\in\{0,1\}. \] The characteristic-zero qualification does not cover positive-characteristic group rings.
Manuscript 4.
For any discrete group $G$, any integer $q\ge1$, and any idempotent matrix $e\in M_q(\ell^1(G))$, write $\tau_C(e)$ for the sum, on a conjugacy class $C$, of the coefficients of its diagonal trace. The claim is that some finite set $F$ of finite-order conjugacy classes satisfies \[ C\notin F\quad\Longrightarrow\quad\tau_C(e)=0. \] Equivalently, the $\ell^1$ Hattori--Stallings trace has image in the algebraic direct sum on torsion conjugacy classes. No claim about arbitrary positive-characteristic fields follows from this complex Banach-algebra statement.

Outline of the argument

Finite labeled graphs encode supports whose product coefficients cancel modulo two. A random-label counting argument excludes planar path arrangements; cone surgeries turn that exclusion into asphericity and root separation, so the coefficients remain nonzero in a torsion-free group. An unequal-side parity pattern supplies the one-sided inverse relation in labeled graphs. Weighted counts handle repeated edge traversals, and a separator reduces arbitrarily large planar arrangements to bounded path collections; cone attachment and root separation then preserve the inverse defect while proving torsion-freeness.

An idempotent is encoded by finite cyclic path configurations whose weighted deletion relations generate cycles. Exterior differential forms and a cyclic Pfaffian identity detect forbidden conjugacy support; trace-rank arguments then turn the complex trace conclusion into the stated idempotent consequence. Analytic idempotent correction first replaces the matrix, up to similarity, by one with exponential decay. Weighted cyclic configurations are then treated with smooth spatial summaries, multiscale time averages, and an ordered-kernel estimate; one class-independent cutoff proves actual finite support rather than only absolute summability.

Formal verification

For family 196, the documented Lean theorem includes the torsion-free characteristic-two zero product, finite presentation, and a finite two-dimensional classifying model. The listed Comparator files are TorsionFreeZeroDivisors.lean. Named declarations include OAI.TorsionFreeZeroDivisors.main. For family 197, the documented Lean entries include the scalar inverse defects in the specified characteristics and an operator-invertible determinant counterexample. The characteristic-two search recipe is included, but the nonsofic consequence, the extra spectral-integral conclusion, and the later torsion-free construction are outside the selected statements. No Comparator is assigned to the selected manuscript here; the family page selects other papers or supporting statements. For family 207, the documented Lean statements give complex group-ring Bass trace support and characteristic-zero torsion-free trace rank and idempotent triviality. The separate $\ell^1$ theorem is not selected. The listed Comparator files are BassTorsionFree.lean, BassTrace.lean. Named declarations include OAI.BassTrace.RightProjective.bassTraceModules_vanishing_and_support. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources