we-solve (beta)

Math-2488-A1 · revision r1 · on Math-2488

OpenAI claim summary for Math-2488

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 universal-group theorem embeds every finitely presented group into an $F_\infty$ group, hence into an $F_3$ group. This resolves the first clause of the recorded question. It does not establish the analogous embedding for every group of type $\mathrm{FP}_2$, which need not be finitely presented, or supply the requested totally disconnected locally compact analogue. The simple-overgroup companion assumes decidable word problem and adds no answer to those missing clauses. The bundle remains partial.

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

Manuscript

Contents
  1. Higher Finiteness Embeddings and TDLC Analogues
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Result 1.
  5. Result 2.
  6. Outline of the argument
  7. Formal verification
  8. Status caveat
  9. Sources

Higher Finiteness Embeddings and TDLC Analogues

OpenAI's claim

The linked manuscripts present the following claims by OpenAI: One group of type $F_\infty$ is claimed to contain every finitely presented group, with finitely generated subgroups exactly the recursively presented ones; A group with finitely many generators and a decidable identity-word test is claimed to embed into a nontrivial simple group of type $F_\infty$. Together they provide the following support within the scopes described below.

Mathematical statement of the claimed result

Result 1.
The claimed group $H$ has type $F_\infty$, meaning a classifying space with finite skeleton in every dimension, and satisfies \[ \forall G\text{ finitely presented},\qquad\exists\iota:G\hookrightarrow H. \] The corollary characterizes the finitely generated subgroups embeddable in this same $H$: \[ G\text{ finitely generated}:\qquad G\hookrightarrow H \quad\Longleftrightarrow\quad G\text{ recursively presented}. \] This does not assert embedding of every countable group.
Result 2.
Consider a group $G$ generated by finitely many elements, with an algorithm deciding its word problem. The assertion supplies a nontrivial simple group $H$ of type $F_\infty$ and an embedding \[ \iota:G\hookrightarrow H. \] Type $F_\infty$ requires finite skeleta of a classifying space in all dimensions. The decidability condition on $G$ is part of this theorem.

Outline of the argument

A universal finite presentation is inserted into faithful finite diagram envelopes using two systems of idempotents. An ascending-torus construction supplies uniform fillings with finitely many simplex types in each dimension, establishing the claimed higher finiteness of the universal envelope.

Encoded finite diagrams carry faithful actions with controlled stabilizers. A homological device for ascending tori provides fillings in every dimension, and stabilizers of finite type in a highly transitive action assemble the simple overgroup while retaining higher finiteness.

Formal verification

For family 250, the documented entries cover Boone--Higman equivalence, simple $F_\infty$ overgroups for decidable word problems, and one universal $F_\infty$ group. The converse characterization of all its recursively presented subgroups is extra manuscript scope. The listed Comparator files are BooneHigman.lean, SimpleOvergroups.lean, UniversalFInfinity.lean. Named declarations include OAI.UniversalFInfinity.universal_group_of_type_FInfinity. 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