Problems / erdos-1050 / erdos-1050--h1
Borwein approximants to T (untyped binders)
erdos-1050--h1
superseded
Left open by a proof skeleton.
Superseded by erdos-1050--h1-v2. Work continues on the replacement; this statement is kept for its history (D-8). The curator's record: superseded by erdos-1050--h1-v2 on revision request targets/erdos-1050/nodes/erdos-1050--h1/revisions/20260917T215432Z-calib-lead-83dd.yaml (other-with-exhibit; D-8)
$\displaystyle \exists\, a,b:\ \bigl(\forall n\in\mathbb{N},\ b_n\,T-a_n\neq 0\bigr)\ \wedge\ \lim_{n\to\infty}\bigl(b_n\,T-a_n\bigr)=0,\qquad T=\sum_{m=0}^{\infty}\frac{1}{2^{m+3}-3}$
There are two sequences $a$, $b$ such that $b_n T - a_n$ is never zero and tends to $0$, where $T$ is the sum of $1/(2^{m+3}-3)$ over all $m\ge 0$ (Lean's ∑', with the summation variable also written n in the file). As written, a and b carry no binder types and the sum, the quotient and the coercions ↑ carry no type ascriptions, so the text does not fix the domain of the arithmetic (the display reads it with $a,b:\mathbb{N}\to\mathbb{Z}$ and the sum in $\mathbb{R}$, the types the parent's have borwein carries); the limit is Filter.Tendsto … atTop (nhds 0).
Lean
theorem erdos_1050__h1 : ∃ a b,
(∀ (n : ℕ), ↑(b n) * ∑' (n : ℕ), 1 / (2 ^ (n + 3) - 3) - ↑(a n) ≠ 0) ∧
Filter.Tendsto (fun n => ↑(b n) * ∑' (n : ℕ), 1 / (2 ^ (n + 3) - 3) - ↑(a n)) Filter.atTop (nhds 0) := by
sorryWhy does it end in sorry?
A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
How it is being proved
Superseded.
What is known
Work on it
How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →
Record
Statement: the Lean file and its words (1 version)
Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.
import Mathlib
/-! Hole `borwein` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/
theorem erdos_1050__h1 : ∃ a b,
(∀ (n : ℕ), ↑(b n) * ∑' (n : ℕ), 1 / (2 ^ (n + 3) - 3) - ↑(a n) ≠ 0) ∧
Filter.Tendsto (fun n => ↑(b n) * ∑' (n : ℕ), 1 / (2 ^ (n + 3) - 3) - ↑(a n)) Filter.atTop (nhds 0) := by
sorryA statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle \exists\, a,b:\ \bigl(\forall n\in\mathbb{N},\ b_n\,T-a_n\neq 0\bigr)\ \wedge\ \lim_{n\to\infty}\bigl(b_n\,T-a_n\bigr)=0,\qquad T=\sum_{m=0}^{\infty}\frac{1}{2^{m+3}-3}$
There are two sequences $a$, $b$ such that $b_n T - a_n$ is never zero and tends to $0$, where $T$ is the sum of $1/(2^{m+3}-3)$ over all $m\ge 0$ (Lean's ∑', with the summation variable also written n in the file). As written, a and b carry no binder types and the sum, the quotient and the coercions ↑ carry no type ascriptions, so the text does not fix the domain of the arithmetic (the display reads it with $a,b:\mathbb{N}\to\mathbb{Z}$ and the sum in $\mathbb{R}$, the types the parent's have borwein carries); the limit is Filter.Tendsto … atTop (nhds 0).
Rendered from gloss/3760ab1ed901….md · Improve these words →
Rendered from targets/erdos-1050/nodes/erdos-1050--h1/Statement.lean. Origin: skeleton-hole.
Witness — its slot is open
Not checked — the witness slot is open.
83b3f76974bd./-! The witness slot for a hole (D-29, F07-R6). Replace `sorry` with an instance satisfying this statement's hypotheses; until then the node is blocked. -/ theorem witness : True := by sorry
No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →
How to read this page
No explainer yet. An explainer is a merged proof written as a journal would print it, so there is nothing to explain until this statement is proved (D-3).