we-solve (beta)

Math-1808-A1 · revision r1 · on Math-1808

OpenAI claim summary for Math-1808

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 of type $F_\infty$ contains every finitely presented group, so it supplies the $F_{n+1}$ overgroup for each input of type $F_n$ with $n\ge2$. For a prime $p$, the Prüfer group has the recursive presentation $\langle c_1,c_2,\ldots\mid c_1^p=1,\ c_{i+1}^p=c_i\ (i\ge1)\rangle$. The source gives an HNN construction embedding a countably generated recursively presented group into a finitely generated recursively presented group. Applying that construction here and then Higman embedding places the Prüfer group in a finitely presented group, hence in the universal $F_\infty$ overgroup. Such an overgroup is of type $\mathrm{FP}_\infty$ and therefore $\mathrm{FP}_3$. These consequences cover every clause on this page. The simple-overgroup result has a decidability restriction and is not needed for these deductions.

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

Manuscript

Contents
  1. Questions in Geometric Group Theory — Q 8.7
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Result 1.
  5. Result 2.
  6. Consequences for the two embedding clauses.
  7. Outline of the argument
  8. Formal verification
  9. Status caveat
  10. Sources

Questions in Geometric Group Theory — Q 8.7

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.
Consequences for the two embedding clauses.
If $n\ge2$, type $F_n$ implies finite presentation, so the claimed universal overgroup has type $F_{n+1}$. For each prime $p$, the presentation $C_{p^\infty}=\langle c_1,c_2,\ldots\mid c_1^p=1,\ c_{i+1}^p=c_i\ (i\ge1)\rangle$ is countable and recursive. The source's HNN construction compresses it to a finitely generated recursive presentation. Higman's theorem then gives a finitely presented overgroup, which the claimed universal theorem embeds into an $F_\infty$ group. In particular, the Prüfer group acquires an overgroup of type $\mathrm{FP}_\infty$, and thus of type $\mathrm{FP}_3$. These are deductions from the selected source claim and its stated embedding construction.

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