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

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.

$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]

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).

[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].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

15 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

P. Hackman, Elementary Number Theory, Chapter E, Example E.II.3(b) (standard reference, not scraped)

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