CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

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 common divisors of $(0, 0)$ are all of $Z$ and have no greatest element in the order of $Z$ , so $\gcd (0, 0)$ cannot be defined as a maximum and is fixed by convention

Statement refuted

Refuted claim: for every pair of integers $(a, b)$ the set

$D (a, b) = {d \in Z : d ∣ a and d ∣ b}$

of common divisors has a greatest element, so that $\gcd (a, b)$ can be defined as that maximum at every pair (Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ , Common divisor, and the greatest common divisor $\gcd (a, b)$ , with the convention $\gcd (0, 0) : = 0$ ).

Witness: $(a, b) = (0, 0)$ . Every integer divides $0$ , so $D (0, 0) = Z$ ; and $Z$ has no greatest element, since $m < m + 1$ for every $m$ . So there is no maximum to take, and $\gcd (0, 0)$ is fixed by the convention $\gcd (0, 0) : = 0$ of Common divisor, and the greatest common divisor $\gcd (a, b)$ , with the convention $\gcd (0, 0) : = 0$ rather than computed.

This does not contradict A nonempty set of integers bounded above has a greatest element, and a nonempty set of integers bounded below has a least element: that lemma requires the set to be bounded above, and $Z$ is not.

Facts & Assumptions

Given: The set $D (0, 0)$ of common divisors of $0$ and $0$ .

[L1]

$Z$ is a commutative ring: $x \cdot 0 = 0$ , $x + 0 = x$ , $x \cdot 1 = x$ , $x \cdot (- 1) = - x$ , and every $x$ has an additive inverse (The integers form a commutative ring, Arithmetic on the integers, The integers as equivalence classes of pairs of naturals).

[L2]

The order on $Z$ is total, antisymmetric and transitive and is compatible with addition; positives are closed under multiplication; $x < y$ means $x \leq y$ together with $x \neq y$ (The integers form a totally ordered ring, Order on the integers).

[L3]

$d ∣ u$ means $u = d q$ for some $q$ ; in particular $d ∣ 0$ for every $d$ , since $0 = d \cdot 0$ (Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

[L4]

A nonempty set of integers bounded above has a greatest element (A nonempty set of integers bounded above has a greatest element, and a nonempty set of integers bounded below has a least element).

[L5]

$ι : N \to Z$ is injective with image the nonnegative integers, and $ι (1) = 1$ , $ι (0) = 0$ (The naturals embed in the integers).

[L6]

$d = \gcd (u, v)$ exactly when $d \geq 0$ , $d ∣ u$ , $d ∣ v$ , and every common divisor of $u$ and $v$ divides $d$ (Every common divisor of $a$ and $b$ divides $\gcd (a, b)$ ; consequently $d = \gcd (a, b)$ exactly when $d \geq 0$ , $d ∣ a$ , $d ∣ b$ , and every common divisor of $a$ and $b$ divides $d$ — a characterisation that holds at $(a, b) = (0, 0)$ as well).

Counterexample

technique · direct

1.1

$D (0, 0) = Z$ : every integer $d$ satisfies $d ∣ 0$ , so every integer is a common divisor of $0$ and $0$ .

1.2

$0 < 1$ : $1 = ι (1)$ lies in the image of $ι$ , hence $0 \leq 1$ ; and $1 \neq 0$ because $ι$ is injective and $1 \neq 0$ in $N$ .

2.1

For every $m \in Z$ , $m < m + 1$ : adding $m$ to $0 < 1$ gives $m \leq m + 1$ , and $m = m + 1$ would give $0 = 1$ after adding $- m$ , contrary to step 1.2.

step 1.2L1L2

3.1

$Z$ has no greatest element: if $m$ were one, then $m + 1 \in Z$ would give $m + 1 \leq m$ , while $m < m + 1$ by step 2.1, contradicting antisymmetry.

step 2.1L2

3.2

[L4] is not contradicted, since its hypothesis fails: $Z$ is not bounded above, because for any candidate bound $b$ the integer $b + 1$ exceeds it by step 2.1.

step 2.1L4

4.1

By steps 1.1 and 3.1 the set $D (0, 0)$ has no greatest element, so the refuted claim fails at $(0, 0)$ and no maximum defines $\gcd (0, 0)$ .

step 1.1step 3.1

5.1

What survives at $(0, 0)$ is the divisibility characterisation [L6]: $0 \geq 0$ , $0 ∣ 0$ , and every common divisor of $(0, 0)$ divides $0$ by [L3], so $0$ is the value that characterisation returns — which is exactly the convention adopted in Common divisor, and the greatest common divisor $\gcd (a, b)$ , with the convention $\gcd (0, 0) : = 0$ .

step 4.1L3L6∎

Remarks

The failure is only at $(0, 0)$ . For every other pair one of the two arguments is nonzero, and then the common divisors are bounded above by its absolute value (If $d ∣ a$ and $a \neq 0$ then $d \neq 0$ and $∣ d ∣ \leq ∣ a ∣$ ; hence the set of divisors of a nonzero integer is bounded above by $∣ a ∣$ ), so A nonempty set of integers bounded above has a greatest element, and a nonempty set of integers bounded below has a least element applies and the maximum exists.
The convention is not a patch over an inconvenience but over an absence. There is no integer that could serve as "the greatest common divisor of $0$ and $0$ " in the order of $Z$ , so a value has to be supplied; that it is $0$ is forced by the identities $\gcd$ is required to satisfy ( $\gcd$ at the boundary: $\gcd (a, 0) = ∣ a ∣$ , $\gcd (0, 0) = 0$ , and the convention $\gcd (0, 0) = 0$ is exactly what makes $\gcd (c a, c b) = ∣ c ∣ \gcd (a, b)$ true at $c = 0$ ).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

34 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

Greatest common divisor (Wikipedia) (standard reference, not scraped)
Divisor (Wikipedia) (standard reference, not scraped)

The common divisors of (0,0)(0,0) are all of ZZ and have no greatest element in the order of ZZ, so gcd⁡(0,0)gcd(0,0) cannot be defined as a maximum and is fixed by convention