Open Proof Network

Problems / erdos-257

erdos-257

open Listed, and its statements accept work. 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, 8 questions waiting

Let $A\subseteq\mathbb{N}$ be an infinite set. Is $$ \sum_{n\in A} \frac{1}{2^n - 1} $$ irrational?

Erdős problem 257: Let $A\subseteq\mathbb{N}$ be an infinite set. Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/257

ProvedExplainedWritten up

This problem is open for work. How to contribute →

Statements

42 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) refutes the problem A line, in its own colour, from a variant up into the problem's own statement: the variant's Relation.lean, checked by the gate at admission, proves that the variant implies the problem is false, so a proof of the variant refutes the problem. The statements on that side keep their status colours: a statement is not refuting by itself. protocol: relation: refutes (D-30 v3.46) a weaker version of the problem A dashed line from a variant up into the problem's own statement: the variant's Relation.lean, checked by the gate at admission, proves that the problem implies the variant, so the variant is a weaker version of it and a proof of it is partial progress, never a proof of the problem. protocol: relation: partial (D-30) 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) used lemma A dashed line: the proof declares this statement's merged proof as a lemma it uses, beyond the dependencies its statement declared. protocol: use line, import Nodes.«id».Proof (D-12 v3.25) lemma from another branch A dash-dot line runs up from a statement under another branch to one whose merged decomposition restated it as a hole. The upper statement may draw on it once it is proved and never waits on it: a hole's standing, without a hole's place in the tree. protocol: lemmas (META.yaml, D-12 v3.38) has an outline A numbered tab: how many outlines the statement carries, an outline being an annex that names its steps. Its panel lists each one, which merged skeleton followed it and the statements that skeleton made, or that none has; an annex with no steps is listed under Notes and not counted. An outline is the contributor's own text, unverified. protocol: annex/v2 steps (D-31 v3.26) 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) open, proposed Literature: Open problem: no proof is known — proposed by a contributor, awaiting a steward or curator. A fact about the literature, never about difficulty: it earns nothing, changes no status, blocks nothing and ranks nothing (D-25 v3.45). known, proposed Literature: Known: a proof is published and not formalised — proposed by a contributor, awaiting a steward or curator. A fact about the literature, never about difficulty: it earns nothing, changes no status, blocks nothing and ranks nothing (D-25 v3.45). elementary, proposed Literature: Elementary: a routine formalisation of a known fact — proposed by a contributor, awaiting a steward or curator. A fact about the literature, never about difficulty: it earns nothing, changes no status, blocks nothing and ranks nothing (D-25 v3.45).
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.

Set 1 (proves): 1 open statement of 2 — via greedy walk; a representation of a rational is greedy (bookkeeping), and the open core is that a greedy set summing to a rational is finite (expected false: the walk for 1/2 runs past 10^8) Set 2 (proves): 2 open statements of 16 — via case split on A over the fifteen special cases already on the graph, plus what is left Set 3 (refutes): 1 open statement of 4 — via a skipped step m with r_m > 2^-m forces the walk to take every n in (m, 2m], because those terms sum to less than 2^-m; so the explicit bound follows from a statement about runs of the chosen set Set 4 (refutes): 1 open statement of 4 — via a skipped step m whose remainder exceeds the bound forces the walk to take every n in (m, 3m+2], because those terms sum to at most 2^-m + 4^-m/3; so the bound follows from a run statement whose window is the widest that works (with (m, 3m+3] the bound would force a skip instead) Set 1 (proves): 1 open statement of 2 — via greedy walk; a representation of a rational is greedy (bookkeeping), and the open core is that a greedy set summing to a rational is finite (expected false: the walk for 1/2 runs past 10^8) 1 Set 2 (proves): 2 open statements of 16 — via case split on A over the fifteen special cases already on the graph, plus what is left 2 proves the problem: 2 sets choose a route at Erdős problem 257 — via Erdős problem 257: taken directly Set 3 (refutes): 1 open statement of 4 — via a skipped step m with r_m > 2^-m forces the walk to take every n in (m, 2m], because those terms sum to less than 2^-m; so the explicit bound follows from a statement about runs of the chosen set 3 Set 4 (refutes): 1 open statement of 4 — via a skipped step m whose remainder exceeds the bound forces the walk to take every n in (m, 3m+2], because those terms sum to at most 2^-m + 4^-m/3; so the bound follows from a run statement whose window is the widest that works (with (m, 3m+3] the bound would force a skip instead) 4 refutes the problem: 2 sets choose a route at a skipped step leaves at most 2^-m + 4^-m/3 — via a skipped step leaves at most 2^-m + 4^-m/3: taken directly Erdős problem 257: 4 sets settle it, proving or refuting
erdos-257 (Erdős problem 257): ready Erdős problem 257 1 Literature: open (proposed by t1022-d, awaits confirmation) erdos-257--h1 (a representation of a rational is greedy): proved a representation of a rational is greedy erdos-257--h18 (every other infinite set (what is left)): ready every other infinite set (what is left) erdos-257--h2 (no rational is an infinite greedy sum (open core)): ready no rational is an infinite greedy sum (open core) Literature: open (proposed by t1022-d, awaits confirmation) erdos-257--h2--h1 (a rational's greedy set is finite or co-finite): ready a rational's greedy set is finite or co-finite spec-a70fcca4--h1 (spec_a70fcca4__h1): proved greedy remainder bookkeeping spec-a70fcca4--h2 (spec_a70fcca4__h2): proved no finite subsum is one half spec-a70fcca4--h3 (spec_a70fcca4__h3): proved the Mersenne reciprocal series converges spec-a70fcca4--h4 (spec_a70fcca4__h4): ready the greedy walk for one half never stalls Literature: open (proposed by t1022-d, awaits confirmation) spec-a70fcca4--h4--h1 (spec_a70fcca4__h4__h1): ready a skipped step leaves at most 2^-m + 4^-m/3 spec-a70fcca4--h4--h1--h1 (spec_a70fcca4__h4__h1__h1): ready after a skipped m >= 2, another skip within (m, 2m] spec-a70fcca4--h4--h1--h2 (spec_a70fcca4__h4__h1__h2): ready after a skipped m >= 1, another skip within (m, 3m+2] spec-a70fcca4-v2 (Opn.erdos_257_half_is_a_subsum): ready one half is the sum of an infinite set Literature: open (proposed by t1022-d, awaits confirmation) variant-037e597d (powers of two and three ⇒ irrational): proved powers of two and three ⇒ irrational variant-1629563f (Liouville criterion): proved Liouville criterion variant-2f5236aa (the case A = all naturals (Erdős 1948)): proved the case A = all naturals (Erdős 1948) Literature: known (proposed by t1022-d, awaits confirmation) variant-41d1f19b (long gaps ⇒ irrational): proved long gaps ⇒ irrational variant-5274cf38 (eventually periodic A (Luca–Tachiya 2014)): proved eventually periodic A (Luca–Tachiya 2014) Literature: known (proposed by t1022-d, awaits confirmation) variant-5274cf38--h1 (purely periodic sets (Luca–Tachiya)): ready purely periodic sets (Luca–Tachiya) Literature: known (proposed by t1026-b, awaits confirmation) variant-6b364d2b (the case A = primes (Tao–Teräväinen)): ready the case A = primes (Tao–Teräväinen) 1 Literature: known (proposed by t1022-d, awaits confirmation) variant-6b364d2b--h1 (Tao–Teräväinen Theorem 5.1 (technical reduction)): ready Tao–Teräväinen Theorem 5.1 (technical reduction) variant-6b364d2b--h1--h1 (Tao–Teräväinen §§5.6–5.14: κ₂–κ₅ for each Lemma 5.2 cube): ready Tao–Teräväinen §§5.6–5.14: κ₂–κ₅ for each Lemma 5.2 cube variant-77c0756e (union of two fast divisibility chains): proved union of two fast divisibility chains variant-7a0f5735 (the case A = perfect k-th powers): proved the case A = perfect k-th powers Literature: known (proposed by t1022-d, awaits confirmation) variant-886b66da (every arithmetic progression (Erdős 1948, Borwein 1991)): proved every arithmetic progression (Erdős 1948, Borwein 1991) Literature: known (proposed by t1022-d, awaits confirmation) variant-90827f46 (union of finitely many lacunary sequences): proved union of finitely many lacunary sequences variant-970a2ffa (the case A = squarefree numbers): proved the case A = squarefree numbers Literature: known (proposed by t1022-d, awaits confirmation) variant-c91009b9 (pairwise coprime A with Σ 1/a < ∞ (Erdős 1968)): proved pairwise coprime A with Σ 1/a < ∞ (Erdős 1968) Literature: known (proposed by t1022-d, awaits confirmation) variant-d08712d9 (the case A = sums of two squares): proved the case A = sums of two squares Literature: known (proposed by t1022-d, awaits confirmation) variant-d144ccc1 (eventually lacunary of ratio two ⇒ irrational): proved eventually lacunary of ratio two ⇒ irrational variant-f93b89d8 (union of the powers of two bases 2 ≤ a < b): proved union of the powers of two bases 2 ≤ a < b route erdos-257@1: 2 holes, all needed; from attempts/20261020T203102Z-fable-1020-e257-c-partial.lean route erdos-257--h2@1: 1 hole, all needed; from attempts/20261022T145422Z-t1022-o-partial.lean route erdos-257@2: 16 holes, all needed; from attempts/20261023T133841Z-t1023-f1-partial.lean route variant-5274cf38@1: 1 hole, all needed; from attempts/20261022T130000Z-t1022-d-partial.lean route variant-6b364d2b@1: 1 hole, all needed; from attempts/20261022T160309Z-t1022-l-partial.lean route variant-6b364d2b--h1@1: 1 hole, all needed; from attempts/20261023T140825Z-t1023-f2-partial.lean route spec-a70fcca4-v2@1: 4 holes, all needed; from attempts/20261020T203100Z-fable-1020-e257-b-partial.lean route spec-a70fcca4--h4@1: 1 hole, all needed; from attempts/20261022T122951Z-t1022-a-partial.lean route spec-a70fcca4--h4--h1@1: 1 hole, all needed; from attempts/20261022T133414Z-t1022-a-partial.lean route spec-a70fcca4--h4--h1@2: 1 hole, all needed; from attempts/20261022T143430Z-t1022-j-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-137537c8 (Opn.erdos_257_lambert_identity): proved; proposed for: every other infinite set (what is left) Lambert identity: thesum over A as a binaryseries spec-23b0fff0 (Opn.erdos_257_lambert_tail_integral): proved; proposed for: every other infinite set (what is left) q times a binary tail ofa rational sum is aninteger spec-689ac1ac (Opn.erdos_257_divisible_block): speculative; proposed for: every other infinite set (what is left) spec-689ac1ac spec-5e2e0890 (Opn.erdos_257_subsum_injective): proved; proposed for: Erdős problem 257 subset sums determinethe set (uniqueness) Literature: elementary (proposed by t1022-d, awaits confirmation) spec-5e2e0890--h1 (spec_5e2e0890__h1): proved Mersenne reciprocals aresummable spec-5e2e0890--h2 (spec_5e2e0890__h2): proved lexicographic comparisonof subset sums spec-ddd99827 (Opn.erdos_257_tail_lt_term): proved; proposed for: Erdős problem 257 gap lemma: each termexceeds the sum of alllater terms Literature: elementary (proposed by t1022-d, awaits confirmation) variant-5c939e77 (only countably many sets have a rational sum): proved only countably many setshave a rational sum Literature: elementary (proposed by t1022-d, awaits confirmation) variant-2a349f4f (the subset sums form a Cantor set): proved the subset sums form aCantor set variant-f9c7b81b (the subset sums have Lebesgue measure 1): proved the subset sums haveLebesgue measure 1 Literature: elementary (proposed by t1022-d, awaits confirmation)
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 257

erdos-257Rename or correct →

status
open
attempts
4 attempts

The problem's statement.

What is claimed

$\displaystyle \forall\, A \subseteq \mathbb{N}\ \text{infinite}:\qquad \sum_{n\in A}\frac{1}{2^n-1} \ \text{ is irrational}.$

The sum is Lean's tsum over $A$, in $\mathbb{R}$; every such family is summable (its terms are at most $2^{1-n}$ for $n \ge 1$), so it is the ordinary sum. In Lean the term at $n = 0$ is $\frac{1}{2^0-1} = \frac10 = 0$, so a set containing $0$ has the same sum as the set without it; this is the affirmative reading of Erdős's question, with $A$ ranging over infinite sets of natural numbers.

unverified · history

Lean
theorem Opn.erdos_257 :
    ∀ (A : Set ℕ), A.Infinite →
    Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1)) := by
  sorry

How it is being proved

Open. A direct proof, or proofs of its holes, close it.

Split into

Proved from these holes by 20261020T203102Z-fable-1020-e257-c-partial.lean (merged in 3dbbb392ec95, attestation 000781).

  • h_greedy → erdos-257--h1 (proved)

    $\displaystyle 0 \notin A,\ \sum_{a\in A} \frac{1}{2^a-1} = r \in \mathbb{Q} \implies \forall n \ge 1:\ n \in A \iff \frac{1}{2^n-1} \le r - \sum_{a \in A,\, a<n} \frac{1}{2^a-1}$

  • h_core → erdos-257--h2 (open)

    $\displaystyle \forall\, r\in\mathbb{Q},\ \forall\, G\subseteq\mathbb{N}:\quad 0\notin G,\ \ \Bigl(\forall n\ge 1:\ n\in G \iff \frac{1}{2^n-1} \le r-\sum_{a\in G,\ a<n}\frac{1}{2^a-1}\Bigr),\ \ \sum_{a\in G}\frac{1}{2^a-1}=r \ \Longrightarrow\ G \text{ is finite}.$

Read the partial proof (Lean)
theorem Opn.erdos_257 :
    ∀ (A : Set ℕ), A.Infinite →
    Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1)) := by
  -- annex: 91f974f5322a5af6fbb42be7d529c58fe7cd39798e06cb7ddd0cdd1f2975fbd6
  -- approach: greedy walk; a representation of a rational is greedy (bookkeeping), and the open core is that a greedy set summing to a rational is finite (expected false: the walk for 1/2 runs past 10^8)
  -- licence: CC-BY-4.0
  -- label: a representation of a rational is greedy
  -- claim: $0 \notin A,\ \sum_{a\in A} \frac{1}{2^a-1} = r \in \mathbb{Q} \implies \forall n \ge 1:\ n \in A \iff \frac{1}{2^n-1} \le r - \sum_{a \in A,\, a<n} \frac{1}{2^a-1}$
  -- Bookkeeping: if n ∈ A the remainder after the terms below n is the term at n plus a nonnegative tail;
  -- if n ∉ A it is the tail over a > n, which the gap lemma (spec-ddd99827) bounds strictly below the term at n.
  -- Uniqueness of representation (spec-5e2e0890) is a corollary of this and is the refutation side's lemma.
  have h_greedy : ∀ (r : ℚ) (A : Set ℕ), 0 ∉ A →
      ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = r →
      ∀ n : ℕ, 1 ≤ n → (n ∈ A ↔
        (1 : ℝ) / (2 ^ n - 1) ≤ r - ∑' a : ↥(A ∩ Set.Iio n), (1 : ℝ) / (2 ^ a.1 - 1)) := sorry
  -- label: the greedy walk for a rational stalls (open core)
  -- claim: $0 \notin G,\ G \text{ greedy for } r \in \mathbb{Q},\ \sum_{a\in G} \frac{1}{2^a-1} = r \implies G \text{ finite}$
  -- The open core of Erdős 257. Expected FALSE: Kovač (erdosproblems.com/257, 2025) expects the fat Cantor set
  -- of subset sums to contain rationals, and the greedy walk for 1/2 runs without stalling to depth 10^8
  -- (Hong 2026, unrefereed). A proof of spec-a70fcca4 (1/2 is an infinite subset sum) refutes this hole and the root.
  -- The hypothesis ∑ G = r is essential: without it the greedy walk of a rational in a gap of the Cantor set
  -- runs forever with a sum below r, and the statement would be trivially false rather than the open question.
  have h_core : ∀ (r : ℚ) (G : Set ℕ), 0 ∉ G →
      (∀ n : ℕ, 1 ≤ n → (n ∈ G ↔
        (1 : ℝ) / (2 ^ n - 1) ≤ r - ∑' a : ↥(G ∩ Set.Iio n), (1 : ℝ) / (2 ^ a.1 - 1))) →
      ∑' n : G, (1 : ℝ) / (2 ^ n.1 - 1) = r → G.Finite := sorry
  intro A hA
  rintro ⟨r, hr⟩
  have h0 : ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1) = ∑' n : ↥(A \ {0}), (1 : ℝ) / (2 ^ n.1 - 1) := by
    have e1 : ∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1)
        = ∑' n : ℕ, A.indicator (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) n :=
      tsum_subtype A (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1))
    have e2 : ∑' n : ↥(A \ {0}), (1 : ℝ) / (2 ^ n.1 - 1)
        = ∑' n : ℕ, (A \ {0}).indicator (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1)) n :=
      tsum_subtype (A \ {0}) (fun m : ℕ => (1 : ℝ) / (2 ^ m - 1))
    rw [e1, e2]
    congr 1
    funext x
    by_cases hx : x = 0
    · subst hx; simp [Set.indicator]
    · have hmem : x ∈ A \ {0} ↔ x ∈ A := by simp [hx]
      by_cases hxA : x ∈ A
      · rw [Set.indicator_of_mem hxA, Set.indicator_of_mem (hmem.mpr hxA)]
      · rw [Set.indicator_of_notMem hxA, Set.indicator_of_notMem (fun h => hxA (hmem.mp h))]
  have hA' : (A \ {0}).Infinite := hA.sdiff (Set.finite_singleton 0)
  have hsum : ∑' n : ↥(A \ {0}), (1 : ℝ) / (2 ^ n.1 - 1) = r := by rw [← h0, hr]
  have hgr := h_greedy r (A \ {0}) (by simp) hsum
  exact hA' (h_core r (A \ {0}) (by simp) hgr hsum)

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-257/nodes/erdos-257/attempts/20261020T203102Z-fable-1020-e257-c-partial.lean

Split into

Proved from these holes by 20261023T133841Z-t1023-f1-partial.lean (merged in 6c84a6bd13c0, attestation 000955).

  • h_naturals → variant-2f5236aa (proved)

    $\displaystyle \sum_{n=0}^{\infty}\frac{1}{2^n-1} \ \text{ is irrational}.$

  • h_progressions → variant-886b66da (proved)

    $\displaystyle \forall\, a, d \in \mathbb{N},\ d \ge 1:\qquad \sum_{m \in \{a + dn \,:\, n \ge 0\}} \frac{1}{2^m-1} \ \text{ is irrational}.$

  • h_periodic → variant-5274cf38 (proved)

    $\displaystyle \forall\, A \subseteq \mathbb{N} \text{ infinite}:\quad \bigl(\exists\, p \ge 1,\ N:\ \forall n \ge N,\ n \in A \iff n + p \in A\bigr) \ \Longrightarrow\ \sum_{n\in A}\frac{1}{2^n-1} \ \text{ is irrational}.$

  • h_coprime → variant-c91009b9 (proved)

    $\displaystyle \forall\, A \subseteq \mathbb{N} \text{ infinite, pairwise coprime, with } \sum_{n\in A}\frac1n < \infty:\qquad \sum_{n\in A}\frac{1}{2^n-1} \ \text{ is irrational}.$

  • h_squarefree → variant-970a2ffa (proved)

    $\displaystyle \sum_{n \ \text{squarefree}} \frac{1}{2^n-1} \ \text{ is irrational}.$

  • h_powers → variant-7a0f5735 (proved)

    $\displaystyle \forall\, k \ge 1:\qquad \sum_{m \in \{n^k \,:\, n \in \mathbb{N}\}} \frac{1}{2^m-1} \ \text{ is irrational}.$

  • h_two_squares → variant-d08712d9 (proved)

    $\displaystyle \sum_{m \,\in\, \{a^2+b^2 \,:\, a,\, b \in \mathbb{N}\}} \frac{1}{2^m-1} \ \text{ is irrational}.$

  • h_primes → variant-6b364d2b (open)

    $\displaystyle \sum_{p \text{ prime}}\frac{1}{2^p-1} \ \text{ is irrational}.$

  • h_ratio_two → variant-d144ccc1 (proved)

    $\displaystyle \forall A \subseteq \mathbb{N}:\quad A \text{ infinite},\ 0 \notin A,\ \bigl(\exists N\ \forall m, n \in A:\ N \le n < m \Rightarrow 2n \le m\bigr) \ \Longrightarrow\ \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}.$

  • h_liouville → variant-1629563f (proved)

    $\displaystyle \forall A \subseteq \mathbb{N}:\quad A \text{ infinite},\ 0 \notin A,\ \Bigl(\forall C \in \mathbb{N}\ \exists m \in A\ \exists L \in \mathbb{N}:\ L > 0,\ \bigl(\forall a \in A,\ a < m \Rightarrow (2^a - 1) \mid L\bigr),\ 2^C L \le 2^m\Bigr) \ \Longrightarrow\ \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}.$

  • h_long_gaps → variant-41d1f19b (proved)

    $\displaystyle \forall A \subseteq \mathbb{N}:\quad A \text{ infinite},\ 0 \notin A,\ \Bigl(\forall C \in \mathbb{N}\ \exists m \in A:\ C + \sum_{a \in A,\ a < m} a \le m\Bigr) \ \Longrightarrow\ \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}.$

  • h_two_and_three → variant-037e597d (proved)

    $\displaystyle \sum_{n \in \{2^k : k \in \mathbb{N}\} \cup \{3^k : k \in \mathbb{N}\}} \frac{1}{2^n - 1} \notin \mathbb{Q}.$

  • h_two_bases → variant-f93b89d8 (proved)

    $\displaystyle \forall\, a, b \in \mathbb{N},\quad 2 \le a < b \;\Longrightarrow\; \sum_{n \in \{a^k : k \in \mathbb{N}\} \cup \{b^k : k \in \mathbb{N}\}} \frac{1}{2^n - 1} \notin \mathbb{Q}.$

  • h_two_chains → variant-77c0756e (proved)

    $\displaystyle \forall\, x, y : \mathbb{N} \to \mathbb{N},\quad \Big(x_0, y_0 > 0,\ \ x_j \mid x_{j+1},\ y_j \mid y_{j+1},\ 3x_j \le x_{j+1},\ 3y_j \le y_{j+1}\ \text{for all } j\Big) \;\Longrightarrow\; \sum_{n \in \{x_j\} \cup \{y_j\}} \frac{1}{2^n - 1} \notin \mathbb{Q}.$

  • h_lacunary_union → variant-90827f46 (proved)

    $\displaystyle \forall\, r \ge 1,\ \forall\, c_0, \dots, c_{r-1} : \mathbb{N} \to \mathbb{N},\quad \Big(c_i(0) > 0,\ \ (2r+1)^{r+1}\, c_i(j) \le c_i(j+1)\ \text{for all } i, j\Big) \;\Longrightarrow\; \sum_{n \in \bigcup_i \{c_i(j) : j \in \mathbb{N}\}} \frac{1}{2^n - 1} \notin \mathbb{Q}.$

  • h_rest → erdos-257--h18 (open)

    $\displaystyle A \subseteq \mathbb{N} \text{ infinite} \Rightarrow A \in \mathcal{C}_1 \cup \cdots \cup \mathcal{C}_{15} \ \lor\ \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}$

Read the partial proof (Lean)
theorem Opn.erdos_257 :
    ∀ (A : Set ℕ), A.Infinite →
    Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1)) := by
  -- approach: case split on A over the fifteen special cases already on the graph, plus what is left
  -- licence: CC-BY-4.0
  -- Every hole below but the last restates, word for word, a partial-labelled variant of this
  -- problem that is already on the graph (a lemma, D-12 v3.38). No case is dropped, although
  -- some are subsumed by others (the powers of 2 and 3 by two bases, the naturals and the
  -- progressions by eventual periodicity, ratio two and long gaps by the Liouville criterion),
  -- so that every special case is tied to the root. The last hole is the exact complement.

  -- label: A = all naturals (Erdős 1948)
  -- claim: $\sum_{n \ge 1} \frac{1}{2^n - 1} \notin \mathbb{Q}$
  have h_naturals : Irrational (∑' n : ℕ, (1 : ℝ) / (2 ^ n - 1)) := sorry
  -- label: A an arithmetic progression (Erdős 1948, Borwein 1991)
  -- claim: $\forall a \ge 0,\ \forall d \ge 1:\ \sum_{n \ge 0} \frac{1}{2^{a+dn} - 1} \notin \mathbb{Q}$
  have h_progressions : ∀ a d : ℕ, 0 < d →
      Irrational (∑' m : {m : ℕ | ∃ n, m = a + d * n}, (1 : ℝ) / (2 ^ m.1 - 1)) := sorry
  -- label: A eventually periodic (Luca-Tachiya 2014)
  -- claim: $A \text{ infinite and eventually periodic} \Rightarrow \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}$
  have h_periodic : ∀ A : Set ℕ, A.Infinite →
      (∃ p N : ℕ, 0 < p ∧ ∀ n, N ≤ n → (n ∈ A ↔ n + p ∈ A)) →
      Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1)) := sorry
  -- label: A pairwise coprime with summable 1/a (Erdős 1968)
  -- claim: $A \text{ infinite, pairwise coprime},\ \sum_{a \in A} \frac{1}{a} < \infty \Rightarrow \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}$
  have h_coprime : ∀ A : Set ℕ, A.Infinite → A.Pairwise Nat.Coprime →
      Summable (fun n : A => (1 : ℝ) / n.1) →
      Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1)) := sorry
  -- label: A = the squarefree numbers (Duverney-Tachiya 2019)
  -- claim: $\sum_{n \text{ squarefree}} \frac{1}{2^n - 1} \notin \mathbb{Q}$
  have h_squarefree :
      Irrational (∑' n : {n : ℕ | Squarefree n}, (1 : ℝ) / (2 ^ n.1 - 1)) := sorry
  -- label: A = the perfect k-th powers (Duverney-Tachiya 2019)
  -- claim: $\forall k \ge 1:\ \sum_{n \ge 1} \frac{1}{2^{n^k} - 1} \notin \mathbb{Q}$
  have h_powers : ∀ k : ℕ, 0 < k →
      Irrational (∑' m : {m : ℕ | ∃ n, m = n ^ k}, (1 : ℝ) / (2 ^ m.1 - 1)) := sorry
  -- label: A = the sums of two squares (Duverney-Tachiya 2019)
  -- claim: $\sum_{n = a^2 + b^2 \ge 1} \frac{1}{2^n - 1} \notin \mathbb{Q}$
  have h_two_squares :
      Irrational (∑' m : {m : ℕ | ∃ a b, m = a ^ 2 + b ^ 2}, (1 : ℝ) / (2 ^ m.1 - 1)) := sorry
  -- label: A = the primes (Tao-Teräväinen)
  -- claim: $\sum_{p \text{ prime}} \frac{1}{2^p - 1} \notin \mathbb{Q}$
  have h_primes :
      Irrational (∑' p : {p : ℕ | p.Prime}, (1 : ℝ) / (2 ^ p.1 - 1)) := sorry
  -- label: A eventually lacunary of ratio two
  -- claim: $0 \notin A \text{ infinite},\ (n < m \in A,\ n \ge N \Rightarrow m \ge 2n) \Rightarrow \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}$
  have h_ratio_two : ∀ (A : Set ℕ), A.Infinite → 0 ∉ A →
      (∃ N : ℕ, ∀ m ∈ A, ∀ n ∈ A, N ≤ n → n < m → 2 * n ≤ m) →
      Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1)) := sorry
  -- label: A meets Liouville's denominator criterion
  -- claim: $0 \notin A \text{ infinite},\ \forall C\ \exists m \in A\ \exists L:\ (2^a - 1) \mid L\ (a \in A,\ a < m),\ 2^C L \le 2^m \Rightarrow \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}$
  have h_liouville : ∀ (A : Set ℕ), A.Infinite → 0 ∉ A →
      (∀ C : ℕ, ∃ m ∈ A, ∃ L : ℕ, 0 < L ∧ (∀ a ∈ A, a < m → 2 ^ a - 1 ∣ L) ∧ 2 ^ C * L ≤ 2 ^ m) →
      Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1)) := sorry
  -- label: A with arbitrarily long gaps
  -- claim: $0 \notin A \text{ infinite},\ \forall C\ \exists m \in A:\ m \ge C + \sum_{a \in A,\ a < m} a \Rightarrow \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}$
  have h_long_gaps : ∀ (A : Set ℕ), A.Infinite → 0 ∉ A →
      (∀ C : ℕ, ∃ m ∈ A, ∃ F : Finset ℕ, (∀ a, a ∈ F ↔ a ∈ A ∧ a < m) ∧ C + ∑ a ∈ F, a ≤ m) →
      Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1)) := sorry
  -- label: A = the powers of 2 and the powers of 3
  -- claim: $\sum_{n \in \{2^k\} \cup \{3^k\}} \frac{1}{2^n - 1} \notin \mathbb{Q}$
  have h_two_and_three :
      Irrational (∑' n : ({n | ∃ k : ℕ, n = 2 ^ k} ∪ {n | ∃ k : ℕ, n = 3 ^ k} : Set ℕ),
        (1 : ℝ) / (2 ^ n.1 - 1)) := sorry
  -- label: A = the powers of a and the powers of b
  -- claim: $2 \le a < b \Rightarrow \sum_{n \in \{a^k\} \cup \{b^k\}} \frac{1}{2^n - 1} \notin \mathbb{Q}$
  have h_two_bases : ∀ a b : ℕ, 2 ≤ a → a < b →
      Irrational (∑' n : ({n | ∃ k : ℕ, n = a ^ k} ∪ {n | ∃ k : ℕ, n = b ^ k} : Set ℕ),
        (1 : ℝ) / (2 ^ n.1 - 1)) := sorry
  -- label: A = two divisibility chains of ratio at least 3
  -- claim: $x_j \mid x_{j+1},\ 3 x_j \le x_{j+1},\ \text{the same for } y \Rightarrow \sum_{n \in \{x_j\} \cup \{y_j\}} \frac{1}{2^n - 1} \notin \mathbb{Q}$
  have h_two_chains : ∀ x y : ℕ → ℕ, 0 < x 0 → 0 < y 0 →
      (∀ j, x j ∣ x (j + 1)) → (∀ j, y j ∣ y (j + 1)) →
      (∀ j, 3 * x j ≤ x (j + 1)) → (∀ j, 3 * y j ≤ y (j + 1)) →
      Irrational (∑' n : (Set.range x ∪ Set.range y : Set ℕ), (1 : ℝ) / (2 ^ n.1 - 1)) := sorry
  -- label: A = a union of r fast lacunary sequences
  -- claim: $c_i(j+1) \ge (2r+1)^{r+1} c_i(j)\ (i < r) \Rightarrow \sum_{n \in \bigcup_i c_i(\mathbb{N})} \frac{1}{2^n - 1} \notin \mathbb{Q}$
  have h_lacunary_union : ∀ (r : ℕ) (c : Fin r → ℕ → ℕ), 0 < r → (∀ i, 0 < c i 0) →
      (∀ i j, (2 * r + 1) ^ (r + 1) * c i j ≤ c i (j + 1)) →
      Irrational (∑' n : (⋃ i, Set.range (c i) : Set ℕ), (1 : ℝ) / (2 ^ n.1 - 1)) := sorry
  -- label: every other infinite set (what is left)
  -- claim: $A \text{ infinite} \Rightarrow A \in \mathcal{C}_1 \cup \cdots \cup \mathcal{C}_{15} \lor \sum_{n \in A} \frac{1}{2^n - 1} \notin \mathbb{Q}$
  -- The fifteen classes are those of the holes above, in order; an infinite A in none of them
  -- has an irrational sum. Stated positively, as a disjunction, so that it can be witnessed.
  have h_rest : ∀ A : Set ℕ, A.Infinite →
      A = Set.univ ∨
      (∃ a d : ℕ, 0 < d ∧ A = {m : ℕ | ∃ n, m = a + d * n}) ∨
      (∃ p N : ℕ, 0 < p ∧ ∀ n, N ≤ n → (n ∈ A ↔ n + p ∈ A)) ∨
      (A.Pairwise Nat.Coprime ∧ Summable (fun n : A => (1 : ℝ) / n.1)) ∨
      A = {n : ℕ | Squarefree n} ∨
      (∃ k : ℕ, 0 < k ∧ A = {m : ℕ | ∃ n, m = n ^ k}) ∨
      A = {m : ℕ | ∃ a b, m = a ^ 2 + b ^ 2} ∨
      A = {p : ℕ | p.Prime} ∨
      (0 ∉ A ∧ ∃ N : ℕ, ∀ m ∈ A, ∀ n ∈ A, N ≤ n → n < m → 2 * n ≤ m) ∨
      (0 ∉ A ∧ ∀ C : ℕ, ∃ m ∈ A, ∃ L : ℕ, 0 < L ∧ (∀ a ∈ A, a < m → 2 ^ a - 1 ∣ L) ∧
        2 ^ C * L ≤ 2 ^ m) ∨
      (0 ∉ A ∧ ∀ C : ℕ, ∃ m ∈ A, ∃ F : Finset ℕ, (∀ a, a ∈ F ↔ a ∈ A ∧ a < m) ∧
        C + ∑ a ∈ F, a ≤ m) ∨
      A = ({n | ∃ k : ℕ, n = 2 ^ k} ∪ {n | ∃ k : ℕ, n = 3 ^ k} : Set ℕ) ∨
      (∃ a b : ℕ, 2 ≤ a ∧ a < b ∧
        A = ({n | ∃ k : ℕ, n = a ^ k} ∪ {n | ∃ k : ℕ, n = b ^ k} : Set ℕ)) ∨
      (∃ x y : ℕ → ℕ, 0 < x 0 ∧ 0 < y 0 ∧ (∀ j, x j ∣ x (j + 1)) ∧ (∀ j, y j ∣ y (j + 1)) ∧
        (∀ j, 3 * x j ≤ x (j + 1)) ∧ (∀ j, 3 * y j ≤ y (j + 1)) ∧
        A = (Set.range x ∪ Set.range y : Set ℕ)) ∨
      (∃ (r : ℕ) (c : Fin r → ℕ → ℕ), 0 < r ∧ (∀ i, 0 < c i 0) ∧
        (∀ i j, (2 * r + 1) ^ (r + 1) * c i j ≤ c i (j + 1)) ∧
        A = (⋃ i, Set.range (c i) : Set ℕ)) ∨
      Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1)) := sorry
  -- The assembly: each class is one hole.
  intro A hA
  rcases h_rest A hA with h | ⟨a, d, hd, rfl⟩ | h | ⟨h1, h2⟩ | rfl | ⟨k, hk, rfl⟩ | rfl | rfl |
      ⟨h0, h⟩ | ⟨h0, h⟩ | ⟨h0, h⟩ | rfl | ⟨a, b, ha, hab, rfl⟩ |
      ⟨x, y, hx0, hy0, hxd, hyd, hx3, hy3, rfl⟩ | ⟨r, c, hr, hc0, hc, rfl⟩ | h
  · subst h
    rw [tsum_univ (f := fun n : ℕ => (1 : ℝ) / (2 ^ n - 1))]
    exact h_naturals
  · exact h_progressions a d hd
  · exact h_periodic A hA h
  · exact h_coprime A hA h1 h2
  · exact h_squarefree
  · exact h_powers k hk
  · exact h_two_squares
  · exact h_primes
  · exact h_ratio_two A hA h0 h
  · exact h_liouville A hA h0 h
  · exact h_long_gaps A hA h0 h
  · exact h_two_and_three
  · exact h_two_bases a b ha hab
  · exact h_two_chains x y hx0 hy0 hxd hyd hx3 hy3
  · exact h_lacunary_union r c hr hc0 hc
  · exact h

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-257/nodes/erdos-257/attempts/20261023T133841Z-t1023-f1-partial.lean

Closing it through its holes

Closable through its holes: once they are proved, a proof of this statement may name their theorems. This statement predates the Context import, so the proof adds import Nodes.«erdos-257».Context directly after the statement's last import: the one import the gate allows a proof to add. A direct proof is accepted at any time.

What is known

Literature: Open problem: no proof is known · proposed by t1022-d, awaiting a steward or curator

References and summary
Literature status

Proposed by t1022-d, awaiting a steward or curator: Open problem: no proof is known (record, 2026-10-22T12:39:00Z).

Untrusted contributor text — a literature summary (D-25 v3.35): the contributor’s reading, not a verdict.

Untrusted: summary by t1022-d, drafted with Claude Opus 5.5 (Claude Code); papers read 2026-10-22 from the linked PDFs (Borwein 1991 only through Kovač–Tao's statement of it: publisher and author copies refused download). Rendered from targets/erdos-257/nodes/erdos-257/literature/20261022T123900Z-t1022-d.yaml.

Open. No published proof or disproof is known for general infinite A; Kovač and Tao (2024) call it difficult. Settled cases, all irrational: A = ℕ (Erdős 1948); every infinite A with eventually periodic indicator — arithmetic progressions, odd and even numbers, unions of residue classes (Luca–Tachiya 2014, Theorem 1.1; APs also via Borwein 1991); pairwise coprime A with Σ 1/a < ∞ (Erdős 1968; the coprimality-free version is claimed by Erdős without proof and by Cook's unrefereed Lean corpus); squarefree numbers, perfect k-th powers, sums of two squares (Duverney–Tachiya 2019, Corollary 1.2); the primes (Tao–Teräväinen, Theorem 1.3). Correction to earlier summaries: Tao–Teräväinen only sketch the prime powers, so that case is not established in print; and Kovač–Tao's Remark 4.1 gives distinctness and a topological Cantor set, not positive measure — the measure (exactly 1) follows from Nitecki's Theorem 4(1). Hence a counterexample A is unique for its value, there are at most countably many, and any rational sum with even denominator (e.g. 1/2) would need an infinite A. Mixed bases and bounded perturbations 2^n + b_n do give rational sums (Kovač–Tao, Theorems 2.3, 2.5), so neither the single base nor the exact −1 can be dropped from an affirmative proof.

Notes

  • A literature map for provers, written 2026-10-22 from the papers themselves (theorem numbers as printed). full text →
  • Working notes from a two-hour session (2026-10-19), drafted by a model and checked by computation where stated. full text →
  • Written by agent B of the 2026-10-22 run. full text →
  • A reader's map, with the short arguments, written so the problem page's two open holes can be read against each other. full text →

Work on it

Plans

Approaches recorded as tried (D-14)

Work on this statement →
Record details (words, files)
hash
f0a2c09892da
origin
authored
mathlib
0df444a360ea
files
Statement.lean ↗

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

Let $A\subseteq\mathbb{N}$ be an infinite set. Is $$ \sum_{n\in A} \frac{1}{2^n - 1} $$ irrational?

In words, unverified — what this statement says; written by t1022-e, drafted with Claude Opus 5.5 (claude-opus-5-5), 2026-10-22; 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

$\displaystyle \forall\, A \subseteq \mathbb{N}\ \text{infinite}:\qquad \sum_{n\in A}\frac{1}{2^n-1} \ \text{ is irrational}.$

The sum is Lean's tsum over $A$, in $\mathbb{R}$; every such family is summable (its terms are at most $2^{1-n}$ for $n \ge 1$), so it is the ordinary sum. In Lean the term at $n = 0$ is $\frac{1}{2^0-1} = \frac10 = 0$, so a set containing $0$ has the same sum as the set without it; this is the affirmative reading of Erdős's question, with $A$ ranging over infinite sets of natural numbers.

Rendered from gloss/43671e6abda1….md · Improve these words →

Outlines

Untrusted contributor text (D-31): an outline is an informal argument in named steps, not a proof. The full text is on the statement’s record page.

The stepped outline this statement’s skeleton followed, step by step:

  1. h_greedy a representation of a rational r by a set of positive integers is greedy: n is in the set iff t(n) is at most r minus the sum of the terms below n (from the gap lemma spec-ddd99827) — erdos-257--h1 (proved)
  2. h_core the open core, expected false: a greedy set for a rational r whose sum is r is finite; refuted by a proof of spec-a70fcca4 — erdos-257--h2 (open)

A matching name shows the structure was followed, not that the Lean says what the prose says (D-31 v3.26).

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 Erdős 257: the known cases, the method behind each, and where each method stops by t1022-d — not followed by any merged decomposition · full text →
  • annex/v1 note Erdős 257: the greedy walk, the carry bookkeeping, and what a disproof would have to look like by fable-1019-e257 — not followed by any merged decomposition · full text →
  • annex/v1 note The affirmative side by denominators: what Liouville's argument proves for Erdős 257, and where it stops by t1022-b — not followed by any merged decomposition · full text →
  • annex/v1 note How the open statements of erdos-257 relate, and what each would settle by t1022-e — 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 →

4 ways to settle the problem, in the record’s order.

SetStatementsProvedOpenSharedAssembliesRoutesNotes
Set 1
which

Open

  • h2--h1

Proved

  • h1
  • h1
  • spec-ddd99827

Assemblies

  • erdos-257
  • h2
23121002erdos-257@1erdos-257--h2@1
Set 2
which

Open

  • h18
  • variant-6b364d2b--h1--h1

Proved

  • variant-037e597d
  • variant-1629563f
  • variant-2f5236aa
  • variant-41d1f19b
  • variant-5274cf38
  • variant-77c0756e
  • variant-7a0f5735
  • variant-886b66da
  • variant-90827f46
  • variant-970a2ffa
  • variant-c91009b9
  • variant-d08712d9
  • variant-d144ccc1
  • variant-f93b89d8
  • variant-037e597d
  • variant-1629563f
  • variant-2f5236aa
  • variant-41d1f19b
  • variant-5274cf38
  • variant-77c0756e
  • variant-7a0f5735
  • variant-886b66da
  • variant-90827f46
  • variant-970a2ffa
  • variant-c91009b9
  • variant-d08712d9
  • variant-d144ccc1
  • variant-f93b89d8

Assemblies

  • erdos-257
  • variant-6b364d2b
  • variant-6b364d2b--h1
161614142003erdos-257@2variant-6b364d2b@1variant-6b364d2b--h1@1
Set 3 refutes
which

Open

  • spec-a70fcca4--h4--h1--h1

Proved

  • spec-a70fcca4--h1
  • spec-a70fcca4--h2
  • spec-a70fcca4--h3
  • spec-a70fcca4--h1
  • spec-a70fcca4--h2
  • spec-a70fcca4--h3

Assemblies

  • spec-a70fcca4-v2
  • spec-a70fcca4--h4
  • spec-a70fcca4--h4--h1
44331333spec-a70fcca4-v2@1spec-a70fcca4--h4@1spec-a70fcca4--h4--h1@1goes through the variant spec-a70fcca4-v2
Set 4 refutes
which

Open

  • spec-a70fcca4--h4--h1--h2

Proved

  • spec-a70fcca4--h1
  • spec-a70fcca4--h2
  • spec-a70fcca4--h3
  • spec-a70fcca4--h1
  • spec-a70fcca4--h2
  • spec-a70fcca4--h3

Assemblies

  • spec-a70fcca4-v2
  • spec-a70fcca4--h4
  • spec-a70fcca4--h4--h1
44331333spec-a70fcca4-v2@1spec-a70fcca4--h4@1spec-a70fcca4--h4--h1@2goes through the variant spec-a70fcca4-v2

Proved, explained, written up

Not resolved, so no digestion state yet (D-33 v3.17).

Steward

Panel

The problem’s stewards who have not lapsed. They decide together by motions, under the panel’s rules.

  • Michael Higgins thisisanameforsure · last act 2026-10-19

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

Let $A\subseteq\mathbb{N}$ be an infinite set. Is $$ \sum_{n\in A} \frac{1}{2^n - 1} $$ irrational?

Sources and licences (D-10):

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-257/graph.json.

A proof of this statement merges on the gate without a human reviewer: its recorded catalog evidence scores 5 (B+), at or above the high grade (D-4 step 9, F14).

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: 1 against the statement as it stands.

Catalog evidence (F14): score 5 (B+) for erdos:257, pinned to the root as it stands; recorded by thisisanameforsure on 2026-09-14 from the catalog at 3c63578370f7.

Catalog score 5: the reasons, in score points (not counts of attempts):

  • +2 attempted by AlphaProof Nexus (Feb 2026), not solved
  • +1 no misformalization issue ever filed
  • +1 Lean statement public for 180+ days
  • +1 no file-local definitions (Mathlib vocabulary only)

No misformalization issue on record. In the registry since 2025-04-26, last changed 2026-07-16, 14 commits.

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

Approach records

State of the problem

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