---

Beker, On a problem of Erdős and Graham about consecutive sums in strictly increasing sequences, arXiv:2311.10087 (posted 16 November 2023); Bull. London Math. Soc. 56 (2024), no. 8, 2749–2759 (online 28 May 2024); the statements below are cited from arXiv v1. For a finite sequence $a$ let $S(a)$ be the set of its sums $\sum_{u\le i\le v}a_i$ over nonempty blocks of consecutive terms. Theorem 1.2 states that there is an absolute $c_1>0$ such that for every $n$ there are integers $1\le a_1<\cdots<a_k\le n$ with $|S(a)|\ge c_1n^2$; this answers Problem 356 yes, for every $n$ rather than only for large $n$. Theorem 1.3 obtains it from the random sequence $a_i=3i+\epsilon_i$ with independent signs $\epsilon_i$, and Theorem 1.4 from the explicit sequences $a_i=2i-1$, except $a_i=2i$ when $b$ divides $i$, for $\log n\le b\le n/(\log n)^2$; both proofs bound the additive energy of the set of partial sums by a constant multiple of its minimum. Proposition 1.5 shows the trivial bound $n(n+1)/2$ is not sharp: $|S(a)|\le(c_4+o(1))n^2$ with $c_4=(e^2-1)/(2(e^2+1))$. The paper's digest is the library card, which cites arXiv v1 (16 November 2023) and records the statements of its pp. 1–2 without examining the proofs. Konieczny's theorem on permutations of $\{1,\ldots,n\}$, which the site cites beside this result, concerns the variant without monotonicity (Problem 34) and is not a claim on this question.

Accepted: the result is refereed (Bulletin of the London Mathematical Society), and Thomas Bloom, the site's curator, records the original problem as solved in the affirmative by Beker, with the page's thanks to the author (erdosproblems.com/356, page last edited 16 October 2025, accessed 2026-10-07). Nothing here is this project's own review.

Formalization. The file src/latest/ErdosProblems/Erdos356.lean of Boris Alexeev's public repository plby/lean-proofs (added 2026-08-17; 1,189 lines at the pinned commit, the main head of 2026-09-15) declares itself a formalization of this result: its header names Beker as the informal author and Codex and GPT-5.6 Sol as the formal authors. It defines consecutiveSums a for $a:\mathrm{Fin}\,k\to\mathbb N$ as the finite set of sums over nonempty blocks of consecutive terms, and states erdos_356: there is $c>0$ such that for all sufficiently large $n$ there are $k$ and a strictly increasing $a$ with $1\le a_i\le n$ and $c\,n^2\le|\mathrm{consecutiveSums}\,a|$. The proof supplies $c=1/300000$ and, by its docstring, follows Beker's explicit construction with partial sums $t^2+\lfloor t/b\rfloor$ and $b$ the integer square root, through a finite collision-energy estimate imported from a sibling development of the repository; the file prints its axioms with #print axioms and contains no sorry. The community database recorded the problem's formal status as Lean on 2026-08-24, which is the site's LEAN suffix; the repository's record of the file is the record link above. The file was not built or audited by this corpus, so it gives no formalized evidence: the registrations record that a Lean proof exists, not an examination of its statement's fidelity to the problem.