we-solve (beta)

Math-1800-A1 · revision r1 · on Math-1800

OpenAI claim summary for Math-1800

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 main 116-generator example refutes the broader finite-rank/proper-target version. It is not a spherical-type counterexample, so the separately requested finite-type version remains unanswered. This entry records partial support; complete coverage of the question is not established by this catalogue.

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

Manuscript

Contents
  1. Questions in Geometric Group Theory — Q 2.16
  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

Questions in Geometric Group Theory — Q 2.16

OpenAI's claim

OpenAI presents a mathematical result relevant to this question in the selected manuscript. A specific Artin group on 116 generators is claimed to have no proper cocompact isometric action on a proper CAT$0$ space.

Mathematical statement of the claimed result

Result 1.
For an Artin matrix $M$ on 116 generators with off-diagonal entries only in $\{2,3,\infty\}$, the constructed Artin group $A_M$ is claimed to have no action that is simultaneously isometric, proper, and cocompact on any nonempty proper CAT$0$ metric space. In quantified form, \[ \nexists X,\ A_M\curvearrowright X:\quad X\text{ proper CAT}(0),\quad\text{action proper and cocompact}. \] The metric space is required to be proper, and the exclusion is independent of dimension.

Outline of the argument

Stable translation lengths and centralizer characters impose quantitative braid constraints. Six asymptotic sectors and labeled triangular diagrams yield a local winding count incompatible with those constraints; a finite Artin matrix realizes the contradictory configuration.

Formal verification

For family 254, the scope includes finite-rank Salvetti contractibility, the 116-generator Artin CAT$0$ counterexample, and arbitrary parabolic intersections with closure consequences. Each has its own Comparator statement. The listed Comparator files are ArtinCAT0.lean, ArtinParabolicIntersections.lean, HarmonicArtin.lean. Named declarations include OAI.ArtinCAT0.main, OAI.HarmonicArtin.salvetti_cover_contractible. 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