ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

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.

$A_{4}$ is not nilpotent

Example

The group $A_{4}$ has a normal Klein four Sylow $2$ -subgroup and four nonnormal Sylow $3$ -subgroups. Consequently $A_{4}$ is not nilpotent. See Sylow and maximal-subgroup characterizations of finite nilpotence.

Facts & Assumptions

Given: The hypotheses and objects in the Example.

[L1]

For a finite group $G$ , the following are equivalent: $G$ is nilpotent; every Sylow subgroup is normal; $G$ is the internal direct product of its Sylow subgroups; and every maximal subgroup of $G$ is normal. (Sylow and maximal-subgroup characterizations of finite nilpotence).

[L2]

For $n \in N$ , the alternating group is the kernel of the sign homomorphism, $A_{n} : = \ker (sgn : S_{n} \to {+ 1, - 1}) = {σ \in S_{n} : sgn (σ) = 1} .$ Thus $A_{n}$ consists exactly of the even permutations. The subgroup and normality assertions implicit in the word “group” follow from thm-image-subgroup-and-kernel-normal. (The alternating group $A_{n} = \ker (sgn)$ of even permutations).

[L3]

A Sylow $p$ -subgroup of a finite group is normal if and only if it is the unique Sylow $p$ -subgroup. (A Sylow $p$ -subgroup is normal if and only if it is unique).

Verification

technique · direct

1.1

The eight $3$ -cycles in $A_{4}$ occur in four inverse pairs, so they generate four distinct subgroups of order $3$ . These are all the Sylow $3$ -subgroups.

L1L2L3givenalgebra

2.1

Since there is more than one Sylow $3$ -subgroup, none is normal and the Sylow characterization rules out nilpotence. By contrast, the identity together with the three double transpositions is a conjugation-invariant Klein four group, hence the normal Sylow $2$ -subgroup. This proves the stated claim.

step 1.1givenalgebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 63 results over 12 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Keith Conrad, Consequences of the Sylow Theorems, Sections 1-5 (standard reference, not scraped)

A4A4​ is not nilpotent