---

Claim. The answer to Problem 1213 is yes, with an explicit threshold. Let $f(a,K)$ be the largest last term of an increasing integer sequence $a=a_1<\cdots<a_s$ with consecutive gaps at most $K$ in which all sums over nonempty intervals of consecutive indices are distinct. Theorem 3 of N. Hegyvári, On consecutive sums in sequences, states

$$f(a,K)<\Bigl(a+\frac K2\Bigr)e^{K+1}+Ke^{2K+2},$$

so every such sequence whose last term exceeds this bound has two distinct intervals with the same sum. The paper calls these interval sums $c$-sums and attributes the question to Erdős by personal communication; two equal $c$-sums are two distinct, possibly overlapping intervals of equal sum, exactly the question's conclusion, and the bound is of the shape $f(a,K)\ll ae^{O(K)}$ that the site's commentary reports. The proof is a one-page count of short blocks with sum below a threshold $D$, which the paper asserts exceed $D$ in number once $D$ passes the bound, so that two of them share a value (the problem page records a gap in the printed step and its repair). The theorem's statement is on the library's result page.

Depends on. Nothing in this wiki; the theorem is the paper's own.

Acceptance. Refereed: Acta Mathematica Hungarica 48 (1986), no. 1--2, 193--200, doi:10.1007/BF01949064, received October 2, 1984; the Crossref record dates the print issue to March 1986, and the page's name uses the first of that month. Reviewed: the site's curator, Thomas Bloom, labels the problem proved and credits the resolution to [He86], the page's only source (the site's page was last edited 10 April 2026); the community database records the problem proved, with a formalized statement and formal status unformalized (database copy of 2026-10-06). Lean: the catalog google-deepmind/formal-conjectures holds ErdosProblems/1213.lean, which states the question as erdos_1213 with answer(True) and a sorry body, carries a variants.hegyvari statement of the $ae^{O(K)}$ bound, and points its formal_proof attribute at the file src/latest/ErdosProblems/Erdos1213.lean of Boris Alexeev's lean-proofs repository. That file (Lean v4.33.0, Mathlib v4.33.0; pinned at its revision of 2026-09-15, first added on 2026-08-17), linked above with its record page, declares itself a formalization of Hegyvári's solution, naming him as informal author and Codex and GPT-5.6 Sol as formal authors, and proves erdos_1213 without sorry; but its explicit bound is $4^Ka+2K(4^K)^2$, obtained by a sliding-window pigeonhole argument of its own, not Theorem 3's bound or proof. Nothing was built, replayed or audited here, no axiom output is recorded, and no outside reviewer has published an examination, so formalized is not listed.

Not covered. Whether the exponential dependence on $K$ can be lowered: the site attributes to the author the belief that it can, and the paper prints no such remark. Lower bounds for $K\ge2$: the paper gives only the four small values $f(1,1)=2$, $f(2,1)=4$, $f(1,2)=7$, $f(2,2)=10$ and the $K=1$ estimate $a+(1+o(1))2\sqrt a<f(a,1)<a+(1+o(1))5\sqrt a$ for large $a$.