ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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.

The primitive roots modulo $17$ are $3, 5, 6, 7, 10, 11, 12, 14$

Example

The primitive roots modulo $17$ are

$3, 5, 6, 7, 10, 11, 12, 14.$

Facts & Assumptions

Given: The prime modulus $17$ .

[L1]

A unit is a primitive root modulo $n$ when its order is $φ (n)$ (Primitive roots modulo $n$ ).

[L2]

$φ (17) = 16$ ( $φ (1) = 1$ , and $φ (p) = p - 1$ for every prime $p$ ).

[L3]

If $g$ generates a cyclic group of order $m$ , its generators are $g^{a}$ for the exponent classes coprime to $m$ (The generators of a cyclic group of order $m$ are the $g^{a}$ with $\gcd (a, m) = 1$ , so there are $φ (m)$ of them).

Verification

technique · direct

1.1

The successive powers of $3$ modulo $17$ for exponents $1$ through $16$ are $3, 9, 10, 13, 5, 15, 11, 16, 14, 8, 7, 4, 12, 2, 6, 1$ , with no earlier $1$ . Thus $3$ has order $16 = φ (17)$ and is primitive by [L1].

L1L2algebra

2.1

The exponent classes coprime to $16$ are $1, 3, 5, 7, 9, 11, 13, 15$ ; selecting these entries from step 1.1 gives $3, 10, 5, 11, 14, 7, 12, 6$ , which is the displayed set after sorting.

step 1.1L3algebra∎

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: 61 results over 16 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

William Stein, Elementary Number Theory, Example 2.5.13 (standard reference, not scraped)

The primitive roots modulo 1717 are 3,5,6,7,10,11,12,143,5,6,7,10,11,12,14