False statementConstruction: Literature-sourcedVerification: AI-generatedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

All finite simple groups are alternating or cyclic

Statement

Every finite simple group is cyclic or alternating.

Facts & Assumptions

Given: The explicitly constructed finite group $G = PSL (2, 7)$ of PSL(2,7) is a nonabelian simple group of order 168.

[L1]

$G$ is simple, nonabelian, and has order $168$ , by the elementary local proof in PSL(2,7) is a nonabelian simple group of order 168.

[L2]

For $n \geq 2$ , $∣ A_{n} ∣ = n! / 2$ , and $A_{0}, A_{1}$ are trivial ( $A_{n}$ is normal in $S_{n}$ ; for $n \geq 2$ , $2 ∣ A_{n} ∣ = n!$ , while $A_{n} = S_{n}$ for $n = 0, 1$ ).

Refutation

technique · direct

1.1L1L2algebra

By L1, $G$ is finite simple and is not cyclic, since every cyclic group is abelian: powers of one generator commute. By L2 the orders of $A_{n}$ for $0 \leq n \leq 5$ are $1, 1, 1, 3, 12, 60$ . For $n \geq 6$ they are at least $6! / 2 = 360$ , since each further factorial factor is positive and at least one. None equals $168$ , so $G$ is not isomorphic to any alternating group.

2.1step 1.1contradiction∎

Thus $G$ is a finite simple group that is neither cyclic nor alternating, refuting the statement with a fully local construction and simplicity proof.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Stephen D. Smith, CFSG—A User’s Manual (standard reference, not scraped)