we-solve (beta)

Math-2293 · mathematics · Group theory

Finitely presented infinite simple amenable groups

Status Partially solved · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
$\mathbb N$, $\mathbb Z$, $\mathbb Q$, $\mathbb R$, and $\mathbb C$ denote the natural numbers, integers, rationals, reals, and complex numbers, respectively. All additional parameters and hypotheses are specified in the question.
Statement recorded in the supplied source.
Does there exist an infinite simple amenable group that is finitely presented? A finitely generated example alone is insufficient. The source also proposes the derived subgroup of the full group of the Penrose tiling as a possible construction to test for these properties.

Formulation references: [S1], [S2].

Short English statement

Does there exist an infinite simple amenable group that is finitely presented? A finitely generated example alone is insufficient. The source also proposes the derived subgroup of the full group of the Penrose tiling as a possible construction to test for these properties.

Sources

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2293-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2293

The claimed group simultaneously has infinitude, simplicity, finite presentation, and amenability. These are precisely the four existence properties requested, with no separate construction method imposed on the answer.

Finitely presented infinite simple amenable groups

OpenAI's claim

OpenAI presents a proof in the selected manuscript. An infinite finitely presented amenable simple group is claimed to exist.

Mathematical statement of the claimed result

Result 1.
The existence claim is \[ \exists G:\quad |G|=\infty,\quad G\text{ finitely presented},\quad G\text{ simple},\quad G\text{ amenable}. \] Here simplicity excludes proper nontrivial normal subgroups. Both ordinary finite presentability and infinitude are part of the assertion.

Outline of the argument

Boolean polygons over a quadratic ring define a Stone space and piecewise translation tables. Track and slot comparisons give perfection and simplicity, while finite presentation is obtained from the controlled polygon moves and the translation geometry supplies amenability.

Formal verification

For family 253, the documented entry is the single infinite, finitely presented, simple amenable existence example. The listed Comparator files are SimpleAmenable.lean. Named declarations include OAI.SimpleAmenable.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

Go to contribution →