Open Proof Network

Problems / erdos-1050

erdos-1050

proved Its root statement has a merged proof. Not yet explained or written up. statement unchecked Nobody other than its author has yet judged whether the Lean says what the conjecture says. The kernel cannot decide this; a person must. protocol: fidelity: mechanical-only review: needs an intent signer · 1 candidate, 1 cluster, 9 questions waiting

Erdős Problem 1050. The series $\sum_{n=1}^\infty \frac{1}{2^n - 3}$ is irrational. The source sum runs over $n \ge 1$; as a tsum over ℕ (which starts at $0$) it is reindexed $n \mapsto n + 1$, i.e. $\sum_{n=0}^\infty 1/(2^{n+1} - 3)$.

Erdős problem 1050 (calibration): a known result. Statement from formal-conjectures (FormalConjectures/ErdosProblems/1050.lean) · erdosproblems.com/1050; the record lists no licensed source text.

ProvedExplainedWritten up

Proved: a proof is on the record, so the problem's own statement is closed. 1 statement proposed beneath it is open for work. How to contribute →

A calibration target: a result already known, taken in on the formalization track to exercise the pipeline (Stages v3.17). It counts toward no open-problem claim and needs no steward.

Statements

14 statements. The problem's own statement is the one selected when the page opens. A statement is drawn above the statements it depends on, so the pieces of its proof are below it and a variant that uses it is above it. Select one to see its record.

proved A proof passed all nine checks and was merged. Proved is not the same as explained. protocol: proved open No proof has closed this statement and nothing blocks starting on it. Anyone may work on it now. protocol: ready · on the frontier blocked Waits on other statements, or on a definition that has not been checked yet. Not accepting work. A statement waiting only for its witness is not blocked in this sense: it needs a witness. protocol: blocked route: all of its holes A dot on the way down from a statement to the holes of one merged decomposition of it: the route closes the statement only when every hole beneath the dot is proved (AND). protocol: decompositions[] (D-12), routes (D-25 v3.40) any one route closes it A diamond under a statement that two or more routes, or a resolving variant, could close: any one of them suffices (OR), and so would a direct proof. protocol: routes (D-25 v3.40) depends on A solid line runs up from a statement to one that declared it as a dependency: the upper statement's proof may build on the lower one. protocol: deps (META.yaml) speculative statement A statement not connected to the problem: a speculative statement proposed for it (or its revision), or a related variant, with its own holes, in the column at the right of the drawing. No line joins it to the tree at rest: hover or select it to light the lines the record has measured from it (a proof that uses it, a lemma, a relation). Everything connected to the problem, variants with a checked relation included, is in the tree; a statement lives in one place, never both. protocol: proposed-for record (D-14 v3.26, v3.46)
Ways to settle the problem A way to settle the problem: a sufficient set is a set of statements whose proofs would settle the problem's own statement, either proving it or refuting it through a variant whose relation the gate checked, with the closing proofs of the decomposed statements on the way still to submit: one choice of route at every fork. Each set says which way it settles the problem. The tree under this heading is the navigation device: select a set, a family of sets or one route choice and the drawing shows just that part. protocol: sufficient sets (D-25 v3.40, v3.46; F27)

Each set proves the problem or refutes it. Select a node or an edge to filter the drawing to that part of the proof; select it again to come back.

Proof 1 · root · by t1001-1050a P Set 1 (proves): 0 open statements of 1 1
erdos-1050 (Erdős problem 1050 (calibration): a known result): proved Erdős problem 1050 (calibration): a known result erdos-1050--h1-v2 (Borwein approximants to T): proved Borwein approximants to T erdos-1050--h1-v2--h1 (Irrationality of the tail sum T): ready Irrationality of the tail sum T erdos-1050--h1-v2--h2 (Integrality: b(n)z - a(n) = 9^n W(n) E(n)): proved Integrality: b(n)z - a(n) = 9^n W(n) E(n) erdos-1050--h1-v2--h2--h1 (Numerator integrality (Borwein Lemma 3)): proved Numerator integrality (Borwein Lemma 3) erdos-1050--h1-v2--h3 (Borwein's denominator bound: d^2 <= 2^(3n^2)): proved Borwein's denominator bound: d^2 <= 2^(3n^2) erdos-1050--h1-v2--h4 (Borwein's remainder bound (with the denominator hypothesis)): proved Borwein's remainder bound (with the denominator hypothesis) route erdos-1050@1: 1 hole, all needed; from attempts/20260917T141921Z-calib-1050-fable-partial.lean route erdos-1050--h1-v2@1: 1 hole, all needed; from attempts/20260921T064200Z-tester-1050-2045-partial.lean route erdos-1050--h1-v2@2: 1 hole, all needed; from attempts/20260924T123700Z-t0924-1050-mcp-partial.lean route erdos-1050--h1-v2--h2@1: 1 hole, all needed; from attempts/20260929T194647Z-t0929-1-partial.lean route erdos-1050--h1-v2@3: 2 holes, all needed; from attempts/20260924T123718Z-h0924-1050-http-partial.lean
Speculative statements

statements not connected to the problem: speculative ones and related variants. Hover one for the lines the record measured; click to keep them; click it again, click empty space or press Esc to clear.

spec-180d8b72 (erdos_1050_pade_remainder_bound): proved; proposed for: Borwein's remainder bound (with the denominator hypothesis) Padé remainder boundwithout the denominatorhypothesis spec-1a5ab7c3 (erdos_1050_upper_half_mersenne_clears): proved; proposed for: Borwein's denominator bound: d^2 <= 2^(3n^2) Upper-half Mersenneproduct clears thedenominators spec-440db0f9 (erdos_1050_gauss_binom_two_int): proved; proposed for: Borwein's denominator bound: d^2 <= 2^(3n^2) Gaussian binomial at q =2 is an integer spec-eb1219eb (erdos_1050_hden_small_cases): proved; proposed for: Borwein's denominator bound: d^2 <= 2^(3n^2) Denominator bound at n =5 and n = 7 spec-f2b55478 (erdos_1050_pade_remainder_coeff): proved; proposed for: Borwein approximants to T Padé remaindercoefficient identity spec-ffd3137a (erdos_1050_pade_numerator_closed_form): proved; proposed for: Borwein's denominator bound: d^2 <= 2^(3n^2) Padé numeratorcoefficient closed form
labels drop the problem’s own name (a pill’s title has its full id); hovertap a statement to light its lines; select a set in the tree above to see its tree here
Selected statement Erdős problem 1050 (calibration): a known result

erdos-1050Rename or correct →

status
proved
attempts
2 attempts
proof
On proof 1

The problem's statement.

What is claimed

theorem Opn.erdos_1050 :
    Irrational (∑' n : ℕ, (1 : ℝ) / ((2 : ℝ) ^ (n + 1) - 3)) := by
  sorry

unverified · history This file states the theorem Opn.erdos_1050: the real number $\displaystyle \sum_{n=0}^{\infty} \frac{1}{2^{n+1}-3}$ is irrational.

Explain this →

How it is being proved

Proved by Proof.lean (merged in e80916551a30) · attestation 000326.

Split into

Proved from this hole by 20260917T141921Z-calib-1050-fable-partial.lean (merged in 7963dfe00bd8, attestation 000078).

  • borwein → erdos-1050--h1-v2 (proved)

    $\displaystyle \exists\, a,b:\mathbb{N}\to\mathbb{Z}\ \ \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}$

Read the partial proof (Lean)
theorem Opn.erdos_1050 :
    Irrational (∑' n : ℕ, (1 : ℝ) / ((2 : ℝ) ^ (n + 1) - 3)) := by
  -- annex: ebfc846b7b9ca01cf3880bbde14e6a4909e741934a08f0b4d43f8aa3b2405cb2
  -- Borwein's theorem for the tail T = ∑_{n ≥ 3} 1/(2^n − 3), in Diophantine-approximant form:
  -- integer sequences a, b with b n * T − a n never zero and tending to zero (Borwein 1991, 1992).
  have borwein : ∃ 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
    sorry
  -- The irrationality criterion: a real with such approximants is irrational.
  have criterion : ∀ x : ℝ, (∃ a b : ℕ → ℤ, (∀ n : ℕ, (b n : ℝ) * x - a n ≠ 0) ∧
      Filter.Tendsto (fun n : ℕ => (b n : ℝ) * x - a n) Filter.atTop (nhds 0)) →
      Irrational x := by
    rintro x ⟨a, b, hne, hlim⟩ ⟨r, hr⟩
    subst hr
    have hden : (0 : ℝ) < r.den := by exact_mod_cast r.den_pos
    obtain ⟨N, hN⟩ := (Metric.tendsto_atTop.mp hlim) (1 / r.den) (by positivity)
    have h := hN N le_rfl
    rw [Real.dist_eq, sub_zero] at h
    have hnum : (r : ℝ) * r.den = r.num := by exact_mod_cast Rat.mul_den_eq_num r
    have key : ((b N : ℝ) * r - a N) * r.den = ((b N * r.num - a N * r.den : ℤ) : ℝ) := by
      push_cast
      linear_combination (b N : ℝ) * hnum
    have hz : (b N * r.num - a N * r.den : ℤ) ≠ 0 := by
      intro h0
      have h1 := key
      rw [h0] at h1
      push_cast at h1
      rcases mul_eq_zero.mp h1 with h2 | h2
      · exact hne N h2
      · exact absurd h2 hden.ne'
    have hge : (1 : ℝ) ≤ |((b N * r.num - a N * r.den : ℤ) : ℝ)| := by
      exact_mod_cast Int.one_le_abs hz
    rw [← key, abs_mul, abs_of_pos hden] at hge
    have hlt : |(b N : ℝ) * r - a N| * r.den < 1 / r.den * r.den :=
      mul_lt_mul_of_pos_right h hden
    rw [one_div_mul_cancel hden.ne'] at hlt
    linarith
  have hT : Irrational (∑' n : ℕ, (1 : ℝ) / ((2 : ℝ) ^ (n + 3) - 3)) := criterion _ borwein
  -- The literal series is the tail: its first two terms are −1 and 1.
  have hpos : ∀ n : ℕ, (0 : ℝ) < (2 : ℝ) ^ (n + 3) - 3 := by
    intro n
    have h1 : (1 : ℝ) ≤ (2 : ℝ) ^ n := one_le_pow₀ (by norm_num)
    have : (2 : ℝ) ^ (n + 3) = 8 * 2 ^ n := by ring
    rw [this]
    linarith
  have htail : Summable (fun n : ℕ => (1 : ℝ) / ((2 : ℝ) ^ (n + 2 + 1) - 3)) := by
    refine Summable.of_nonneg_of_le (fun n => ?_) (fun n => ?_)
      (summable_geometric_of_lt_one (by norm_num : (0 : ℝ) ≤ 1 / 2) (by norm_num))
    · exact div_nonneg zero_le_one (hpos n).le
    · rw [one_div_pow]
      refine one_div_le_one_div_of_le (by positivity) ?_
      have h1 : (1 : ℝ) ≤ (2 : ℝ) ^ n := one_le_pow₀ (by norm_num)
      have : (2 : ℝ) ^ (n + 2 + 1) = 8 * 2 ^ n := by ring
      rw [this]
      linarith
  have hsum : Summable (fun n : ℕ => (1 : ℝ) / ((2 : ℝ) ^ (n + 1) - 3)) :=
    (summable_nat_add_iff 2).mp htail
  have hre : (∑' n : ℕ, (1 : ℝ) / ((2 : ℝ) ^ (n + 1) - 3)) =
      ∑' n : ℕ, (1 : ℝ) / ((2 : ℝ) ^ (n + 3) - 3) := by
    rw [← hsum.sum_add_tsum_nat_add 2]
    simp only [Finset.sum_range_succ, Finset.sum_range_zero]
    norm_num
  rw [hre]
  exact hT

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-1050/nodes/erdos-1050/attempts/20260917T141921Z-calib-1050-fable-partial.lean

What is known

Notes

  • Where erdos-1050 stands, and a ready assembly for the root (t0923-1050-b, 2026-09-23). full text →
  • Informal argument for Erdős problem 1050: the irrationality of S = ∑_{n ≥ 0} 1/(2^(n+1) − 3). full text →
  • What remains for erdos-1050 on the record as of 2026-09-29 (graph c5049c97), by t0929-2. full text →

Work on it

Approaches recorded as tried (D-14)

View the proof →
Record details (words, files)
hash
679c2dd5b140
origin
authored
mathlib
0df444a360ea
files
Statement.lean ↗ · attestation ↗ · Proof.lean ↗

Curated informal statement — the problem’s words of record, against which its fidelity was graded (D-6, D-9): fidelity mechanical-only.

Erdős Problem 1050. The series $\sum_{n=1}^\infty \frac{1}{2^n - 3}$ is irrational. The source sum runs over $n \ge 1$; as a tsum over ℕ (which starts at $0$) it is reindexed $n \mapsto n + 1$, i.e. $\sum_{n=0}^\infty 1/(2^{n+1} - 3)$.

In words, unverified — what this statement says; written by t1006-w1, drafted with Claude Opus 5.5 (claude-opus-5-5) in a Claude Code agent session, 2026-10-06; no one has read it against the Lean and signed it. A gloss of a root is not its words of record: the curated statement above is (D-9).

Draft · drafted, by the model named above

This file states the theorem Opn.erdos_1050: the real number $\displaystyle \sum_{n=0}^{\infty} \frac{1}{2^{n+1}-3}$ is irrational.

In detail:

  • The sum is Lean's ∑' over all natural numbers $n = 0, 1, 2, \dots$ (Mathlib's unconditional sum, a tsum). Each term is the real number $1/(2^{n+1}-3)$, computed in $\mathbb{R}$. The terms are $-1, 1, \tfrac{1}{5}, \tfrac{1}{13}, \tfrac{1}{29}, \dots$; the first, at $n = 0$, is $1/(2-3) = -1$.
  • Re-indexed with $m = n+1$, this is the sum $\sum_{m \ge 1} 1/(2^m - 3)$ of Erdős problem 1050. The file's own comment says the statement is imported, as stated, from google-deepmind/formal-conjectures (FormalConjectures/ErdosProblems/1050.lean, Apache-2.0).
  • Irrational x is Mathlib's predicate: $x$ is not equal to $p/q$, read as a real number, for any rational $p/q$.
  • Two Lean conventions do not come into play here, but a reader should know the file leans on neither. Division by zero is defined to be $0$ in Lean; no denominator $2^{n+1}-3$ is zero (it is $-1$ at $n = 0$ and at least $1$ afterwards). And ∑' of a family that is not summable is defined to be $0$; the statement itself does not assert that the series converges, so the claim is about the tsum as Lean defines it. (The series does converge absolutely, since its terms are eventually bounded by a multiple of $2^{-n}$, so the tsum is the ordinary sum; the merged proof checks summability in its step hT.)

The statement has no hypotheses and no free variables. The file imports all of Mathlib; its body is sorry, the placeholder a statement file carries in place of a proof.

Rendered from gloss/27192f22f314….md · Improve these words →

Notes

Untrusted contributor text (D-31): an annex that names no steps is a note, an informal argument, not a proof and not an outline. The full text is on the statement’s record page.

  • annex/v1 note Where erdos-1050 stands, and a ready assembly for the root (t0923-1050-b, 2026-09-23). by t0923-1050-b — not followed by any merged decomposition · full text →
  • annex/v1 note Informal argument for Erdős problem 1050: the irrationality of S = ∑_{n ≥ 0} 1/(2^(n+1) − 3). by calib-1050-fable — followed by 20260917T141921Z-calib-1050-fable-partial.lean: borwein → erdos-1050--h1-v2 (proved) · full text →
  • annex/v1 note What remains for erdos-1050 on the record as of 2026-09-29 (graph c5049c97), by t0929-2. This updates annex b85da506… on this node… by t0929-2 — not followed by any merged decomposition · full text →

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 →

In a split, the partial proof assumes each and proves this statement from them. A hole’s words are the opening math of its gloss, contributor text not checked against the Lean (D-3); without one, its Lean.

How to read this →

1 way to settle the problem, in the record’s order.

SetStatementsProvedOpenSharedAssembliesRoutes
Set 1
which

Proved

  • erdos-1050
  • erdos-1050
  • h1-v2
  • h1-v2--h3
13130000

How it was proved (in words, unverified)

Informal account, unverified — unverified prose about a kernel-checked proof; the opening of the explainer of proof 1, written by t1006-w1, drafted with Claude Opus 5.5 (claude-opus-5-5) in a Claude Code agent session, 2026-10-06.

Overview

The proof is the classical irrationality criterion, applied to a number $T$ for which another node supplies the approximations. Write $T = \sum_{m \ge 0} 1/(2^{m+3}-3)$. Node erdos-1050--h1-v2 states that there are integer sequences $a_n, b_n$ with $b_n T - a_n \neq 0$ for every $n$ and $b_n T - a_n \to 0$. The proof takes those sequences, shows that the root's sum equals $T$, and then argues: if $T = p/q$ were rational, $q(b_n T - a_n) = b_n p - a_n q$ would be a nonzero integer for every $n$ that also tends to $0$, which is impossible. All the depth sits in erdos-1050--h1-v2; this file is short.

Read the whole explainer, each section beside the steps it explains → · How to read a proof page →

Proved, explained, written up

Resolved — undigested. Reported back as: kernel-checked, not yet explained (D-10 v3.17).

0 of 3 proved nodes in the closing proof's dependency closure carry a signed explainer.

No paper or note recorded yet (D-32).

Steward

No stewards: this target is not an open problem (D-6 v3.17).

Panel

No panel yet: the problem’s stewards are its panel, and it has none. How a panel votes, invites and lapses is in the panel’s rules.

Write-up

No write-up has been recorded for this problem yet. Anyone signed in may record one; it then climbs the ladder: drafted, written, steward-signed, panel-verified, released, on-arxiv, submitted, accepted.

Where the statement comes from

Erdős Problem 1050. The series $\sum_{n=1}^\infty \frac{1}{2^n - 3}$ is irrational. The source sum runs over $n \ge 1$; as a tsum over ℕ (which starts at $0$) it is reindexed $n \mapsto n + 1$, i.e. $\sum_{n=0}^\infty 1/(2^{n+1} - 3)$.

Statement from formal-conjectures (FormalConjectures/ErdosProblems/1050.lean) · erdosproblems.com/1050; the record lists no licensed source text.

No statement-QA pass is recorded yet (D-9 v3.12).

Fast check (POST /check, non-authoritative): lean-4.33.1 on AXLE (exact). Rendered from targets/erdos-1050/graph.json.

This problem's statement is settled: a further proof of it merges as an alternate, which no person reviews (D-3 v3.13), and nothing beneath it waits for anyone either (v3.20).

Does the Lean say the conjecture?

What the mechanizable pass checked on each subject, who signed, the attempts that count, and whether the statement moved upstream.

Subjectbacktranslationbriefcompileequivalencescreen-consequencescreen-falsescreen-negationscreen-statement
root————————

Documented external attempts counting toward D-9's M: 0 against the statement as it stands.

No catalog evidence is recorded for this root (F14-R3).

No upstream drift on record (D-10 v3.12).

Approach records

State of the problem

No state-of-the-problem note yet (D-32).