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.

✓ 8 results · all verified · 7 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Sums of Two Squares — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Thue's collision argument gives $73 = 3^{2} + 8^{2}$

Example

The prime $73$ has $27^{2} \equiv - 1 (m o d 73)$ . Thue's collision construction with the square $0 \leq i, j \leq 8$ produces the representation

$73 = 3^{2} + 8^{2} .$

Facts & Assumptions

Given: The prime $p = 73$ and the residue $a = 27$ .

[L1]

If $p$ is prime and $p ∤ a$ , then there are nonzero integers $r, s$ with $∣ r ∣, ∣ s ∣ < \sqrt{p}$ and $r a \equiv s (m o d p)$ (Thue's lemma on small nonzero representatives).

[F1]

A representation of a nonnegative integer $n$ as a sum of two squares is an ordered pair $(x, y) \in Z^{2}$ such that $n = x^{2} + y^{2}$ (Representations and primitive representations as sums of two squares).

Verification

technique · direct

1.1algebra

One has $27^{2} = 729 \equiv - 1 (m o d 73)$ , and $8^{2} = 64 < 73 < 81 = 9^{2}$ , so the maximal integer $h$ with $h^{2} < 73$ is $8$ .

2.1step 1.1L1algebra

In the map $(i, j) \mapsto 27 i - j (m o d 73)$ on $0 \leq i, j \leq 8$ , the distinct pairs $(3, 8)$ and $(0, 0)$ collide because $3 \cdot 27 - 8 = 73$ . Their coordinate differences are $(3, 8)$ , exactly as in [L1].

3.1step 1.1step 2.1L1F1algebra∎

The bounds give $0 < 3^{2} + 8^{2} < 2 \cdot 73$ , and step 2.1 together with $27^{2} \equiv - 1$ makes the sum divisible by $73$ . Directly, $3^{2} + 8^{2} = 9 + 64 = 73$ , so $(3, 8)$ is a representation in the sense of [F1].

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Extended Euclid gives $73 = 3^{2} + 8^{2}$ from the root $27$ of $- 1$

Example

Starting from $27^{2} \equiv - 1 (m o d 73)$ , the Euclidean algorithm yields $73 = 3^{2} + 8^{2}$ without searching the full collision square.

Facts & Assumptions

Given: The congruence $27^{2} \equiv - 1 (m o d 73)$ .

[F1]

Verification

technique · direct

1.1algebra

The Euclidean divisions $73 = 2 \cdot 27 + 19$ and $27 = 19 + 8$ give $8 = 27 - 19 = 3 \cdot 27 - 73$ .

2.1step 1.1algebra

Hence $8 \equiv 3 \cdot 27 (m o d 73)$ , and the given square-root congruence gives $8^{2} \equiv 9 \cdot 27^{2} \equiv - 9 (m o d 73)$ ; therefore $73 ∣ 3^{2} + 8^{2}$ .

3.1step 2.1F1algebra∎

Direct evaluation gives $3^{2} + 8^{2} = 9 + 64 = 73$ , so $(3, 8)$ is a two-square representation of $73$ by [F1].

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Prime factorisation gives two representations of $221$ as a sum of two squares

Example

The factorisation $221 = 13 \cdot 17$ and the two sign variants in the two-square identity give

$221 = 10^{2} + 11^{2} = 14^{2} + 5^{2} .$

Facts & Assumptions

Given: The integers $13$ , $17$ , and their product $221$ .

[F1]

[L1]

For all integers $a, b, c, d$ , $(a^{2} + b^{2}) (c^{2} + d^{2}) = (a c - b d)^{2} + (a d + b c)^{2} = (a c + b d)^{2} + (a d - b c)^{2}$ (The Brahmagupta–Fibonacci two-square identity).

Verification

technique · direct

1.1F1algebra

Directly, $13 = 2^{2} + 3^{2}$ and $17 = 1^{2} + 4^{2}$ .

2.1step 1.1L1algebra

The first sign variant in [L1] gives $221 = (- 10)^{2} + 11^{2} = 10^{2} + 11^{2}$ , since $2 \cdot 1 - 3 \cdot 4 = - 10$ and $2 \cdot 4 + 3 \cdot 1 = 11$ .

2.2step 1.1L1algebra

The second sign variant gives $221 = 14^{2} + 5^{2}$ , since $2 \cdot 1 + 3 \cdot 4 = 14$ and $2 \cdot 4 - 3 \cdot 1 = 5$ .

3.1step 2.1step 2.2F1algebra∎

Both pairs satisfy [F1]. They are essentially different because the unordered absolute-coordinate sets ${10, 11}$ and ${5, 14}$ differ.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

$539 = 7^{2} \cdot 11$ is not a sum of two squares

Statement refuted

Every positive integer is a sum of two integer squares. The integer $539$ is a counterexample.

Facts & Assumptions

Given: The integer $539 = 7^{2} \cdot 11$ .

[F1]

[L1]

If $q \equiv 3 (m o d 4)$ is prime and $q ∣ x^{2} + y^{2}$ , then $q ∣ x$ and $q ∣ y$ (A prime congruent to $3$ modulo $4$ divides both coordinates of a divisible two-square sum).

[L2]

A positive integer $n$ is a sum of two squares if and only if every prime $q \equiv 3 (m o d 4)$ occurs to an even exponent in its canonical prime factorisation (Characterisation of positive integers that are sums of two squares).

Counterexample

technique · direct

1.1algebra

The factorisation $539 = 7^{2} \cdot 11$ contains the prime $11 \equiv 3 (m o d 4)$ to exponent one.

2.1step 1.1F1L1assume-contraalgebradischarge-contradiction

If $539 = x^{2} + y^{2}$ , [L1] would give $11 ∣ x, y$ and hence $11^{2} ∣ 539$ , contrary to step 1.1. Thus no representation in the sense of [F1] exists.

3.1step 1.1L2∎

Equivalently, step 1.1 violates the even-exponent condition in [L2].

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The representations $221 = 5^{2} + 14^{2} = 11^{2} + 10^{2}$ recover the factors $13$ and $17$

Example

The normalized representations

$221 = 5^{2} + 14^{2} = 11^{2} + 10^{2}$

feed the factorisation construction and recover $221 = 13 \cdot 17$ .

Facts & Assumptions

Given: The displayed representations of $221$ .

[F1]

[L1]

For an odd integer, two essentially different normalized representations force a factorisation $N = P Q$ with $P, Q > 1$ (Two essentially different two-square representations factor an odd integer).

Verification

technique · direct

1.1F1algebra

Both equalities are direct, and $(5, 14)$ and $(11, 10)$ are positive odd-even normalized pairs with $0 < 5 < 11$ .

2.1step 1.1L1algebra

In the notation of [L1], the values $e = 2$ , $f = 3$ , $g = 4$ , $h = 1$ give $e g - f h = 5$ , $f g + e h = 14$ , $e g + f h = 11$ , and $f g - e h = 10$ .

3.1step 2.1F1algebra∎

The resulting factors are $e^{2} + f^{2} = 13$ and $g^{2} + h^{2} = 17$ , and $13 \cdot 17 = 221$ .

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The primitive two-square criterion distinguishes $289$ , $34$ , and $833$

Example

The integers $289$ and $34$ have primitive representations, whereas $833$ is representable but has no primitive two-square representation:

$289 = 8^{2} + 15^{2}, 34 = 3^{2} + 5^{2}, 833 = 28^{2} + 7^{2} .$

Facts & Assumptions

Given: The three displayed integers and coordinate pairs.

[F1]

A two-square representation is primitive when its coordinate gcd is $1$ (Representations and primitive representations as sums of two squares).

[L1]

A positive integer $n$ has a primitive two-square representation if and only if $v_{2} (n) \leq 1$ and no prime $q \equiv 3 (m o d 4)$ divides $n$ (Characterisation of primitive sums of two squares).

Verification

technique · direct

1.1F1L1algebra

One has $8^{2} + 15^{2} = 289$ with $\gcd (8, 15) = 1$ , and $3^{2} + 5^{2} = 34$ with $\gcd (3, 5) = 1$ , so both displayed representations are primitive by [F1].

1.2F1algebra

One has $28^{2} + 7^{2} = 833$ , but $\gcd (28, 7) = 7$ , so the displayed representation is not primitive.

2.1step 1.2L1algebra∎

Since $833 = 7^{2} \cdot 17$ and $7 \equiv 3 (m o d 4)$ , [L1] excludes every primitive representation of $833$ , not just the displayed one.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

$68 = 8^{2} + 2^{2}$ is representable but has no primitive two-square representation

Statement refuted

Every integer representable as a sum of two squares has a primitive two-square representation. The integer $68$ is a counterexample.

Facts & Assumptions

Given: The integer $68$ .

[F1]

A two-square representation is primitive when its coordinate gcd is $1$ (Representations and primitive representations as sums of two squares).

[L1]

A positive integer $n$ has a primitive two-square representation if and only if $v_{2} (n) \leq 1$ and no prime $q \equiv 3 (m o d 4)$ divides $n$ (Characterisation of primitive sums of two squares).

Counterexample

technique · direct

1.1F1algebra

Directly, $68 = 8^{2} + 2^{2}$ , but $\gcd (8, 2) = 2$ , so the displayed representation is not primitive.

1.2F1algebra

In any equality $4 k = x^{2} + y^{2}$ , square residues modulo $4$ force both $x$ and $y$ even. Thus no representation of a multiple of four can be primitive.

2.1step 1.1step 1.2L1algebra∎

Since $v_{2} (68) = 2$ , [L1] gives the same conclusion: $68$ has no primitive representation despite step 1.1.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Squarefree sums of two squares up to $30$

Example

Among the squarefree positive integers at most $30$ , those representable as sums of two squares are

$1, 2, 5, 10, 13, 17, 26, 29.$

Every displayed representation below is primitive.

Facts & Assumptions

Given: Positive integers at most $30$ .

[F1]

A two-square representation is primitive when its coordinate gcd is $1$ (Representations and primitive representations as sums of two squares).

[F2]

A positive integer $n$ is squarefree if no square of a prime divides $n$ (Squarefree positive integers).

[L1]

A squarefree positive integer is a sum of two squares if and only if none of its odd prime factors is congruent to $3$ modulo $4$ ; every such representation is primitive (Squarefree sums of two squares).

Verification

technique · direct

1.1F2algebra

Trial division gives the squarefree positive integers at most $30$ as $1, 2, 3, 5, 6, 7, 10, 11, 13, 14, 15, 17, 19, 21, 22, 23, 26, 29, 30$ .

2.1step 1.1L1algebra

Applying [L1] removes exactly those having an odd prime factor congruent to $3$ modulo $4$ , leaving $1, 2, 5, 10, 13, 17, 26, 29$ .

3.1step 2.1F1L1algebra∎

The complete witness list is $1 = 1^{2} + 0^{2}$ , $2 = 1^{2} + 1^{2}$ , $5 = 1^{2} + 2^{2}$ , $10 = 1^{2} + 3^{2}$ , $13 = 2^{2} + 3^{2}$ , $17 = 1^{2} + 4^{2}$ , $26 = 1^{2} + 5^{2}$ , and $29 = 2^{2} + 5^{2}$ . Each coordinate gcd is one, as [F1] and [L1] require.

Sums of Two Squares — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Thue's collision argument gives 73=32+8273=32+82

Example

Facts & Assumptions

Verification

Extended Euclid gives 73=32+8273=32+82 from the root 2727 of −1−1

Example

Facts & Assumptions

Verification

Prime factorisation gives two representations of 221221 as a sum of two squares

Example

Facts & Assumptions

Verification

539=72⋅11539=72⋅11 is not a sum of two squares

Statement refuted

Facts & Assumptions

Counterexample

The representations 221=52+142=112+102221=52+142=112+102 recover the factors 1313 and 1717

Example

Facts & Assumptions

Verification

The primitive two-square criterion distinguishes 289289, 3434, and 833833

Example

Facts & Assumptions

Verification

68=82+2268=82+22 is representable but has no primitive two-square representation

Statement refuted

Facts & Assumptions

Counterexample

Squarefree sums of two squares up to 3030

Example

Facts & Assumptions

Verification

Sources

Thue's collision argument gives $73 = 3^{2} + 8^{2}$

Extended Euclid gives $73 = 3^{2} + 8^{2}$ from the root $27$ of $- 1$

Prime factorisation gives two representations of $221$ as a sum of two squares

$539 = 7^{2} \cdot 11$ is not a sum of two squares

The representations $221 = 5^{2} + 14^{2} = 11^{2} + 10^{2}$ recover the factors $13$ and $17$

The primitive two-square criterion distinguishes $289$ , $34$ , and $833$

$68 = 8^{2} + 2^{2}$ is representable but has no primitive two-square representation

Squarefree sums of two squares up to $30$