ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

Odd primes represented by a divisor of $x^{2} + 3$

Example

An odd prime $p$ divides $x^{2} + 3$ for some integer $x$ if and only if $p = 3$ or $p \equiv 1 (m o d 3)$ . Equivalently, for every odd prime $p \neq 3$ , the congruence $x^{2} \equiv - 3 (m o d p)$ is soluble if and only if $p \equiv 1 (m o d 3)$ .

Facts & Assumptions

Given: An odd prime $p$ .

[L1]

For distinct odd primes $p, q$ , $(\frac{p}{q}) (\frac{q}{p}) = (- 1)^{(p - 1) (q - 1) / 4}$ (Quadratic reciprocity for distinct odd primes).

[L2]

For every odd prime $p$ , $(\frac{- 1}{p}) = (- 1)^{(p - 1) / 2}$ (First supplement: $(- 1 / p) = (- 1)^{(p - 1) / 2}$ ).

[L3]

For an odd prime $p$ , the Legendre symbol is $1$ exactly on the nonzero square classes modulo $p$ (The Legendre symbol, including its zero value).

[L4]

For every odd prime $p$ and integers $a, b$ , $(\frac{a b}{p}) = (\frac{a}{p}) (\frac{b}{p})$ (The Legendre symbol is multiplicative for all integer numerators).

Verification

technique · direct

1.1

Suppose $p \neq 3$ . Applying [L1] to $3$ and $p$ gives $(3 / p) (p / 3) = (- 1)^{(p - 1) / 2} = (- 1 / p)$ by [L2]. Since $(3 / p)$ is a sign and [L4] gives $(- 3 / p) = (- 1 / p) (3 / p)$ , multiplication by $(3 / p)$ yields $(- 3 / p) = (p / 3)$ .

L1L2L4givenalgebra

2.1

By [L3], $x^{2} \equiv - 3 (m o d p)$ is soluble exactly when $(- 3 / p) = 1$ . For $p \neq 3$ , step 1.1 makes this equivalent to $(p / 3) = 1$ , and the nonzero square classes modulo $3$ consist only of $1$ , so this is equivalent to $p \equiv 1 (m o d 3)$ . For $p = 3$ , the class $x = 0$ directly satisfies $x^{2} \equiv - 3 (m o d 3)$ .

step 1.1L3algebra∎

Depends on

Used by

There are infinitely many primes congruent to 1 modulo 3 Corollary

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 48 results over 19 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

A. Gorodnik, Number Theory, Lecture 9, Example 2.4 (standard reference, not scraped)

Odd primes represented by a divisor of x2+3x2+3