we-solve (beta)

Math-118-A2 · revision r1 · on Math-118

OpenAI claim summary for Math-118

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: 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 torsion-free hyperbolic example has one fixed nonidentity element killed by every finite quotient, exactly refuting residual finiteness. Within these assumptions, this is a claimed negative answer to the stated question.

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

Manuscript

Contents
  1. Residual Finiteness of Hyperbolic Groups
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Result 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

Residual Finiteness of Hyperbolic Groups

OpenAI's claim

OpenAI presents a counterexample in the selected manuscript. A torsion-free hyperbolic group is claimed not residually finite and consequently not linear over any field.

Mathematical statement of the claimed result

Result 1.
There is claimed to be a torsion-free word-hyperbolic group $G$ whose finite residual is nontrivial: \[ R_f(G)=\bigcap_{\substack{Q\text{ finite}\\\phi:G\to Q}}\ker\phi\ne\{1\}. \] For this finitely generated example, the linear-obstruction corollary states \[ \forall K\text{ commutative field},\ \forall n\ge1,\ \forall\rho:G\to\operatorname{GL}_n(K),\qquad R_f(G)\subseteq\ker\rho. \] Thus a single nonidentity element is annihilated by every such finite-dimensional representation.

Outline of the argument

Punctured-line blocks with few short cycles give triangular relations meeting a geometric filling criterion. Real and prime-field rank comparisons produce a persistent finite-quotient obstruction, while local factorization certificates and planar metric bounds establish hyperbolicity and exclude torsion.

Formal verification

For family 252, the selected example is torsion-free hyperbolic and fails residual finiteness. Nonlinearity is a further group-theoretic consequence, not a separate selected conclusion. The listed Comparator files are TorsionFreeHyperbolic.lean. Named declarations include OAI.Release075.main. 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