Proving Kimberling's harmonic-floor conjecture

2026-10-25 [home]

This page contains generated content delineated using this shadowing style.

A108211 is the sequence $a (n) = 16 n^{2} + 1$ , starting at $n = 1$ :

17, 65, 145, 257, 401, 577, \dots .

A conjecture of Clark Kimberling from September 2014 gives a different way to obtain these integers:

For every $n \geq 1$ ,
$⌊ \frac{1}{\frac{1}{4 n} - log 2 + H_{2 n} - H_{n}} ⌋ = 16 n^{2} + 1 .$

Here $H_{n} = 1 + 1 / 2 + \dots + 1 / n$ is the $n$ th harmonic number, $log$ is the natural logarithm, and $⌊ x ⌋$ rounds $x$ down to an integer. For example, at $n = 1$ the denominator is $3 / 4 - log 2$ , whose reciprocal lies between $17$ and $18$ .

This conjecture is true. The proof compiles using only propext, Classical.choice, and Quot.sound.

Proof

The definition and theorem statement below omit the proof body:

def a (n : ℕ) : ℕ := 16 * n ^ 2 + 1

theorem kimberling_conjecture (n : ℕ) (hn : 1 ≤ n) :
    ⌊(1 : ℝ) / (1 / (4 * (n : ℝ)) - Real.log 2 +
      ∑ k ∈ Icc (n + 1) (2 * n), (1 : ℝ) / k)⌋
      = (a n : ℤ)

Here Icc (n + 1) (2 * n) includes both endpoints, so the sum is $1 / (n + 1) + \dots + 1 / (2 n)$ , exactly $H_{2 n} - H_{n}$ . The index k simply runs through those denominators, replacing OEIS's written-out sum without changing its value. The divisions take place in the real numbers, and the floor is an integer. The hypothesis hn restricts the claim to $n \geq 1$ , matching the sequence's first index.

Write the denominator as

x_{n} = \frac{1}{4 n} - log 2 + H_{2 n} - H_{n} .

It is enough to prove

\frac{1}{16 n^{2} + 2} < x_{n} < \frac{1}{16 n^{2} + 1} .

Taking reciprocals will then put $1 / x_{n}$ strictly between the consecutive integers $16 n^{2} + 1$ and $16 n^{2} + 2$ .

Comparing consecutive terms

Subtracting consecutive terms cancels $log 2$ and almost all of the harmonic sums:

x_{n} - x_{n + 1} & = \frac{1}{4 n} - \frac{1}{4 (n + 1)} + \frac{1}{n + 1} - \frac{1}{2 n + 1} - \frac{1}{2 n + 2} & = \frac{1}{4 n (n + 1) (2 n + 1)} .

Also, $H_{m} - log m$ converges to the Euler–Mascheroni constant. Consequently,

x_{n} = \frac{1}{4 n} + (H_{2 n} - log (2 n)) - (H_{n} - log n) ⟶ 0 .

Now introduce the two comparison sequences

L_{n} = \frac{1}{16 n^{2} + 2}, U_{n} = \frac{1}{16 n^{2} + 1} .

Both tend to zero. Their consecutive differences trap the difference of $x_{n}$ :

L_{n} - L_{n + 1} < x_{n} - x_{n + 1} < U_{n} - U_{n + 1} (n \geq 1) .

These are exact rational inequalities. To check them, put $D_{n} = 4 n (n + 1) (2 n + 1)$ . Direct subtraction gives

(U_{n} - U_{n + 1}) - \frac{1}{D_{n}} = \frac{32 n^{2} + 32 n - 17}{D_{n} (16 n^{2} + 1) (16 (n + 1)^{2} + 1)} > 0

and

\frac{1}{D_{n}} - (L_{n} - L_{n + 1}) = \frac{36}{D_{n} (16 n^{2} + 2) (16 (n + 1)^{2} + 2)} > 0 .

Every denominator is positive, and both numerators are positive for $n \geq 1$ .

From differences to bounds

The upper comparison says

x_{n} - U_{n} < x_{n + 1} - U_{n + 1} .

Thus $x_{n} - U_{n}$ is strictly increasing. Since it converges to zero, every term must be negative: A nonnegative term would force all later terms to stay above some positive value. Hence

x_{n} < U_{n} = \frac{1}{16 n^{2} + 1} .

Similarly, the lower comparison says

x_{n} - L_{n} > x_{n + 1} - L_{n + 1} .

This difference is strictly decreasing to zero, so every term is positive. Therefore

\frac{1}{16 n^{2} + 2} = L_{n} < x_{n} .

In particular, $x_{n} > 0$ . Taking reciprocals reverses the inequalities and gives

16 n^{2} + 1 < \frac{1}{x_{n}} < 16 n^{2} + 2 .

Rounding down proves

⌊ \frac{1}{x_{n}} ⌋ = 16 n^{2} + 1 (n \geq 1) .

Source

The source code for this proof can be found on my GitHub.

AI Disclosure

These results were obtained primarily using a mix of Anthropic, OpenAI, and open weight models in a private benchmark using a bespoke harness.