ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-09 (gpt-5.6-terra-codex-subscription)

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 harmonic series $\sum 1 / k$ diverges, by condensation and by Oresme block grouping

Example

The harmonic series is $\sum_{k \geq 1} 1 / k$ , the series from the starting index $1$ (Series, partial sums, convergence and the sum, divergence, and the tail series) of the family $a_{k} = 1 / ι (k)$ ; the index $0$ is excluded because $1 / 0$ has no value. It diverges, and its partial sums are unbounded above.

This is the case $p = 1$ of For rational $p > 0$ , $\sum 1 / k^{p}$ converges iff $p > 1$ . The two arguments below do not use that theorem: the first is the condensation argument, which is how For rational $p > 0$ , $\sum 1 / k^{p}$ converges iff $p > 1$ itself is proved and which here degenerates to something one can read off; the second is Oresme's block grouping from the fourteenth century, which uses no test at all and produces the explicit lower bound

$\sum_{k = 1}^{2^{n}} \frac{1}{k} \geq 1 + \frac{n}{2} (n \in N) .$

That bound is worth having on its own: it says the harmonic partial sums grow at least like a constant multiple of $n$ along the powers of $2$ , giving a concrete quantitative witness to their slow divergence.

Facts & Assumptions

Given: The family $a_{k} : = 1 / ι (k)$ for naturals $k \geq 1$ , with $ι (k)$ the canonical natural; its partial sums $A_{m} = \sum_{k = 1}^{m} a_{k}$ (Series, partial sums, convergence and the sum, divergence, and the tail series, Finite sums and finite products, by recursion, Canonical naturals are positive and strictly increasing).

[L1]

The canonical naturals are positive and order preserving: $0 < ι (j) \leq ι (k)$ for $1 \leq j \leq k$ ; and reciprocation reverses the order on the positives (Canonical naturals are positive and strictly increasing, Inverses of positives are positive, and reciprocation reverses order).

[L2]

Condensation: for a nonnegative nonincreasing family from $1$ , $\sum_{k \geq 1} x_{k}$ converges if and only if $\sum_{j \geq 0} 2^{j} x_{2^{j}}$ converges (For a nonincreasing nonnegative sequence, $\sum a_{k}$ converges iff $\sum 2^{k} a_{2^{k}}$ converges, Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences).

[L3]

A series whose terms do not tend to $0$ diverges (If a series converges then its terms tend to $0$ ).

[L4]

Powers of $2$ : $2^{j} \geq 1$ , $2^{j + 1} = 2 \cdot 2^{j}$ , and $2^{j} \cdot (1 / 2^{j}) = 1$ (Integer powers $a^{m}$ , Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ).

[L5]

Splitting and monotonicity of finite sums, and the number of terms in $\sum_{k = p}^{q}$ , namely $q + 1 - p$ (Laws of finite sums and finite products, Finite sums and finite products, by recursion).

[L6]

The principle of induction (The principle of mathematical induction); and for every real $x$ there is a natural $n$ with $ι (n) > x$ (Every complete ordered field is Archimedean).

[L7]

For a series of nonnegative terms: it converges if and only if the range of its partial sums is bounded above (A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum, Lower bound, bounded below, bounded set).

Verification

technique · direct

1.1

Each $a_{k} = 1 / ι (k)$ is positive, and $a_{j} \geq a_{k}$ whenever $1 \leq j \leq k$ , since $0 < ι (j) \leq ι (k)$ and reciprocation reverses the order.

givenL1

1.2

For every $n \in N$ the block $\sum_{k = 2^{n} + 1}^{2^{n + 1}} 1 / k$ has $2^{n + 1} - 2^{n} = 2^{n}$ terms, each with index $k \leq 2^{n + 1}$ and hence each at least $1 / 2^{n + 1}$ ; so the block is at least $2^{n} \cdot \frac{1}{2^{n + 1}} = \frac{1}{2}$ .

L1L4L5

2.1

So the family is nonnegative and nonincreasing, and condensation applies to it.

step 1.1L2

2.2

An induction on $n$ gives $A_{2^{n}} \geq 1 + ι (n) / 2$ for every $n \in N$ . At $n = 0$ it reads $A_{1} = 1 \geq 1$ ; and if it holds at $n$ then, splitting at $2^{n}$ , $A_{2^{n + 1}} = A_{2^{n}} + \sum_{k = 2^{n} + 1}^{2^{n + 1}} 1 / k \geq 1 + ι (n) / 2 + 1 / 2 = 1 + ι (n + 1) / 2$ .

step 1.2L5L6

3.1

The condensed terms are $2^{j} a_{2^{j}} = 2^{j} \cdot \frac{1}{2^{j}} = 1$ for every $j \in N$ .

step 2.1L4

3.2

The range of the partial sums is not bounded above: given a real $M$ , choose a natural $n$ with $ι (n) > 2 M$ ; then $A_{2^{n}} \geq 1 + ι (n) / 2 > 1 + M > M$ .

step 2.2L6choose

4.1

The condensed series is therefore $\sum_{j \geq 0} 1$ , whose terms are constantly $1$ and so do not converge to $0$ ; it diverges.

step 3.1L3

5.1

By condensation, $\sum_{k \geq 1} 1 / k$ diverges. That is the first argument.

step 4.1step 2.1L2

6.1

Since the terms are nonnegative, the series diverges and its partial sums are unbounded above. That is the second argument, and it recovers the conclusion of step 5.1 without using any convergence test.

step 3.2step 1.1L7∎

Remarks

Why the two arguments are the same argument. Oresme's blocks are the blocks of the condensation proof, grouped from $2^{n} + 1$ to $2^{n + 1}$ , and the constant $1 / 2$ in step 1.2 is the constant that makes the condensed terms of step 3.1 equal to $1$ . The difference is bookkeeping: condensation states the grouping once and for all, for every nonincreasing family, and the block argument performs it for this one family.
The divergence is extremely slow, and the bound says how slow. To make the partial sum exceed $M$ the estimate of step 2.2 asks for about $2^{2 M}$ terms. That is why the harmonic series is the standard warning against reading convergence off numerical evidence.
The bound in step 2.2 is one sided. Nothing here says the partial sums are at most $1 + n / 2$ along powers of $2$ , and in fact they are not; the matching upper bound is the other half of the condensation estimate, and it is not needed for divergence.

Depends on

Used by

Dependency tree · two levels

48 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

Harmonic series (mathematics) (Wikipedia) (standard reference, not scraped)
Cauchy condensation test (Wikipedia) (standard reference, not scraped)
John K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)

The harmonic series ∑1/k∑1/k diverges, by condensation and by Oresme block grouping