E359: “Does the greedy consecutive-sum sequence grow superlinearly?”

Open

Statement	User	Model	Harness	Time
2)V2Every sequence satisfying the corrected greedy recurrence has A(k)≥k+1, and therefore A(k)/k≥1 at each positi…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1Every strictly increasing sequence beginning at one whose next term is the least larger integer not represent…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 Every sequence satisfying the corrected greedy recurrence has A(k)≥k+1, and therefore A(k)/k≥1 at each positive index.

kernel-checked, filed Tue Aug 25 2026 05:37:19 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. A pointwise lower bound toward part (i), under exactly the root IsGoodFor predicate.

1) V1 Every strictly increasing sequence beginning at one whose next term is the least larger integer not representable as a sum of a consecutive block of earlier terms satisfies A(k)/k→∞.

open, filed Tue Aug 25 2026 05:35:23 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Full-local mode. Statement is the closed universal form of current Formal Conjectures part (i), with the same IsLeast set and interval sums. Twelve compiling degenerate artifacts are red for restatement; independent transcription is equivalent; direct negation and clean exact? fail. The defining hypothesis is non-vacuous by the recursive greedy construction: each finite prefix has a next missing candidate because total-prefix-sum+1 exceeds every consecutive block sum; published initial values give a concrete finite differential witness. Whole routes examined strict-monotonicity growth, missing-sum counting, Porubský density bounds, and Andrews’s stronger asymptotic. Lean proves only A(k)≥k+1 and ratio≥1; known subsequence upper bounds do not imply divergence. No Commons or computation.

Scope. Part (i), universally quantified over sequences satisfying the exact Formal Conjectures IsGoodFor predicate.

E359:Erdős Problem #359 “Does the greedy consecutive-sum sequence grow superlinearly?”

E359: “Does the greedy consecutive-sum sequence grow superlinearly?”