we-solve (beta)

Math-2709-A1 · revision r1 · on Math-2709

OpenAI claim summary for Math-2709

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 group has a finite generating set and one defining relator. Excluding all Baumslag--Solitar subgroups with both integer parameters nonzero is claimed enough for hyperbolicity, exactly the implication in this question. This is presented as a claimed affirmative answer.

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

Manuscript

Contents
  1. Hyperbolicity of one-relator groups without Baumslag–Solitar subgroups
  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

Hyperbolicity of one-relator groups without Baumslag–Solitar subgroups

OpenAI's claim

OpenAI presents a proof in the selected manuscript. A finitely generated one-relator group without any nontrivial-parameter Baumslag--Solitar subgroup is claimed hyperbolic.

Mathematical statement of the claimed result

Result 1.
Given finite $X$ and $r\in F(X)$, form $G=\langle X\mid r\rangle$. Define \[ \operatorname{BS}(m,n)=\langle a,t\mid ta^mt^{-1}=a^n\rangle \qquad(m,n\in\mathbb Z\setminus\{0\}). \] The source implication is \[ \left(\forall m,n\ne0,\ \operatorname{BS}(m,n)\not\hookrightarrow G\right) \quad\Longrightarrow\quad G\text{ word-hyperbolic}. \] It is restricted to finitely generated one-relator groups.

Outline of the argument

Intersection and commensurator bounds reduce the problem to a restricted HNN setting. Annular diagrams generate a stationary current with finite carriers; failure of expansion would give periodic line trajectories and a forbidden Baumslag--Solitar configuration, completing the hyperbolicity argument.

Formal verification

Family 258 has no Lean scope page in this release. Its selected result is not presented as formalized. 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