Per CONTRIBUTING.md, comments: "ambiguous statement" covers the case where "the literal wording of the statement is easily provable or disprovable or does not match the context of the problem". Problem 265 may qualify.
The statement reads:
Let $1\leq a_1<a_2<\cdots$ be an increasing sequence of integers. How fast can $a_n\to\infty$ grow if $\sum\frac{1}{a_n}$ and $\sum\frac{1}{a_n-1}$ are both rational?
If $a_1 = 1$ then $a_1 - 1 = 0$ and the first term of $\sum \frac{1}{a_n - 1}$ is undefined. The intended reading is presumably $2 \leq a_1$.
This isn't only pedantry about the endpoint: Cantor's example $a_n = \binom{n}{2}$ has to begin at $n = 3$ rather than $n = 2$ for the same reason. With that offset both series are rational, as required — $\sum_{n\geq 3}\frac{1}{\binom{n}{2}} = 1$, and since $\binom{n}{2} - 1 = \frac{(n-2)(n+1)}{2}$ the second telescopes to $\frac{2}{3}\left(1 + \frac12 + \frac13\right) = \frac{11}{9}$.
I'm preparing a Formal Conjectures formalisation and will use 2 ≤ a 0 (which, with StrictMono, gives 2 ≤ a n for all n). Flagging it here first so the divergence from the site's wording is recorded in the open rather than buried in a Lean file.
Two other things I ran into while formalising this, in case they're useful to whoever reviews that PR:
The obvious limsup formulation is a trap. Writing the growth condition as 1 < limsup (fun n => (a n : ℝ) ^ (1 / 2 ^ n)) atTop does not mean what it appears to. Mathlib's Filter.limsup over ℝ unfolds to sInf {b | ∀ᶠ n, f n ≤ b}, and Real.sInf_empty : sInf ∅ = 0, so an unbounded sequence yields the junk value 0 — making the inequality False precisely for the fastest-growing sequences, i.e. exactly inverting the intended meaning. I proved the collapse directly to be sure of it:
theorem limsup_unbounded_junk : limsup (fun n : ℕ => (n : ℝ)) atTop = 0 := by
rw [Filter.limsup, Filter.limSup]
convert Real.sInf_empty
...
The safe form is existential, and needs ∃ᶠ (frequently) rather than ∀ᶠ, since limsup > 1 is an infinitely-often condition — ∀ᶠ would encode the strictly stronger liminf > 1:
def GrowthExceedsOne (a : ℕ → ℕ) : Prop :=
∃ c : ℝ, 1 < c ∧ ∃ᶠ n in atTop, c ^ (2 ^ n) ≤ (a n : ℝ)
Relatedly, the sSup formulation of "how fast can it grow" is only meaningful because the folklore upper bound gives BddAbove; without that hypothesis discharged it would silently collapse the same way. Worth stating as an explicit obligation rather than leaving implicit.
AI disclosure: prepared with AI assistance (GitHub Copilot CLI). The Lean above typechecks against Mathlib v4.30.0 locally; the arithmetic for Cantor's example was checked by hand and numerically.
Per CONTRIBUTING.md,
comments: "ambiguous statement"covers the case where "the literal wording of the statement is easily provable or disprovable or does not match the context of the problem". Problem 265 may qualify.The statement reads:
If$a_1 = 1$ then $a_1 - 1 = 0$ and the first term of $\sum \frac{1}{a_n - 1}$ is undefined. The intended reading is presumably $2 \leq a_1$ .
This isn't only pedantry about the endpoint: Cantor's example$a_n = \binom{n}{2}$ has to begin at $n = 3$ rather than $n = 2$ for the same reason. With that offset both series are rational, as required — $\sum_{n\geq 3}\frac{1}{\binom{n}{2}} = 1$ , and since $\binom{n}{2} - 1 = \frac{(n-2)(n+1)}{2}$ the second telescopes to $\frac{2}{3}\left(1 + \frac12 + \frac13\right) = \frac{11}{9}$ .
I'm preparing a Formal Conjectures formalisation and will use
2 ≤ a 0(which, withStrictMono, gives2 ≤ a nfor alln). Flagging it here first so the divergence from the site's wording is recorded in the open rather than buried in a Lean file.Two other things I ran into while formalising this, in case they're useful to whoever reviews that PR:
The obvious
limsupformulation is a trap. Writing the growth condition as1 < limsup (fun n => (a n : ℝ) ^ (1 / 2 ^ n)) atTopdoes not mean what it appears to. Mathlib'sFilter.limsupoverℝunfolds tosInf {b | ∀ᶠ n, f n ≤ b}, andReal.sInf_empty : sInf ∅ = 0, so an unbounded sequence yields the junk value0— making the inequalityFalseprecisely for the fastest-growing sequences, i.e. exactly inverting the intended meaning. I proved the collapse directly to be sure of it:The safe form is existential, and needs
∃ᶠ(frequently) rather than∀ᶠ, sincelimsup > 1is an infinitely-often condition —∀ᶠwould encode the strictly strongerliminf > 1:Relatedly, the
sSupformulation of "how fast can it grow" is only meaningful because the folklore upper bound givesBddAbove; without that hypothesis discharged it would silently collapse the same way. Worth stating as an explicit obligation rather than leaving implicit.AI disclosure: prepared with AI assistance (GitHub Copilot CLI). The Lean above typechecks against Mathlib v4.30.0 locally; the arithmetic for Cantor's example was checked by hand and numerically.