Erdős Problem 357: bounds on sequences with distinct consecutive sums, formalized in Lean

Let $f(n)$ be the largest $k$ for which there are integers $1 \le a_1 < a_2 < \dots < a_k \le n$ whose consecutive sums $a_i + a_{i+1} + \dots + a_j$ are all different. Erdős and Harzheim asked how $f(n)$ grows, and in particular whether $f(n) = o(n)$: whether such sequences must thin out to a vanishing fraction of $[1, n]$. The question is Erdős Problem 357, and it is open.

Before this work, the best bounds we found were of the form $f(n) \le n/2 + O(\sqrt n)$ (informal, July 2026) and $f(n) \ge (4/\sqrt3 - o(1))\sqrt n$ (a web manuscript). The upper bound $n/2$ comes from a tidy “crossing” argument, and getting below it needs something more.

Results

The upper bound is below $n/2$ only once $n \ge 23{,}202{,}647$, because of its additive constant. What it changes is the leading constant: $\limsup f(n)/n \le 44273/90000$. The constants above are exact. Their decimals are truncated, never rounded up or down to look better.

How the bounds work

Upper bound. Every term whose prefix sum passes $n/2$ owns a block sum in $(n/2, n]$, and these are all different, which gives roughly $n/2$. The new step is a lemma: a short block can be extended one term to the left without its sum exceeding $n$, as long as the sum is at most $(2n+4)/3$. So every integer of $(n/2, 2n/3]$ that is missing from the sequence costs it one term. Missing integers are then forced by a small identity: the $\ell+1$ consecutive integers starting at $\ell w$ have the same sum as the $\ell$ consecutive integers starting at $(\ell+1)w+1$. A valid sequence cannot contain both runs, so at least one of the integers is missing. Five families of such run pairs, arranged so that no integer belongs to more than two of them, force at least $2908$ missing integers per $360000$.

Lower bounds. These build explicit sequences. Six residues modulo 42, $2, 7, 11, 25, 26, 34$, repeated with period 42 and shifted by a large offset, have block sums whose residues determine the block’s length modulo 12. A size argument separates lengths that differ by 12 or more. That gives $12/\sqrt{21}$. Adding 84 to the last fifth of the terms keeps every residue and reduces every possible coincidence to one divisor equation. A counting argument shows that some offset in a window avoids it, which gives $15/\sqrt{21}$. The framework of residue patterns plus a size argument is Pickhardt’s; the pattern, the skip and the proofs are new as far as we found.

How it was checked

The six Lean 4 files prove the theorems for a function f that Lean confirms, by definitional equality, is the f of the Formal Conjectures project’s statement of the problem. They do not prove a weaker variant with a similar name. The checks:

• a clean build with Lean v4.27.0 and Mathlib v4.27.0;
• all 1023 declarations depend only on Lean’s three standard axioms, with no sorry, no native_decide and no added axiom;
• every module replays through lean4checker;
• a script checks every number and finite case in the written proofs with exact arithmetic;
• two AI reviews, one of them adversarial with its own recomputation, found no mathematical error, and every presentation problem they raised was fixed;
• the exact values for $n \le 77$ were reproduced by a third exhaustive search, written without access to the first two.

What “reproduced” means here. These checks were run by AI sessions on the lab’s machine, repeatedly and from clean builds. By this archive’s rules, a result checked only by AI sessions is not marked verified until the author has run the checks personally; that takes one command (below). The entry will be revised when that happens. No human mathematician has checked the proofs, and the paper has not been peer reviewed.

git clone https://github.com/dreadpiratechan/erdos-357
cd erdos-357
FETCH_CACHE=1 bash verification/run_all.sh

The repository’s README explains how to add the kernel replay with lean4checker. On Windows, it says to clone to a short path.

How the results were found

By AI agents, working in a research repository the author set up and directed:

• An OpenAI Codex agent found a modulus-22 predecessor pattern and its Lean proof on 9 September 2026.
• A multi-agent run of Claude models on the night of 22–23 October produced the modulus-42 pattern, the skip, the first upper bounds below $1/2$, and their Lean proofs.
• A further Claude agent produced the five-band design of the final upper bound later on 23 October.
• Claude (Opus 5.5) then wrote the paper and ran the audits.

The author chose the problem, commissioned the runs and decided what to publish. The records show no human contribution to the mathematics itself. The paper’s statement on AI use and the repository’s docs/PROVENANCE.md give the details. The author takes responsibility for the claims on this page and for correcting any that are found to be wrong.

Limits

• Whether $f(n) = o(n)$ is untouched.
• Novelty is not established. No source we found states any of these constants, but two relevant papers were readable only as abstracts or reviews: Hegyvári (1986) and Coppersmith and Phillips (1996). The search is described in the repository’s docs/LITERATURE.md.
• The gain in the upper bound is small, $727/90000 \approx 0.008$ in the leading constant, and the method appears to be near its limit.
• The lower bounds are of order $\sqrt n$, while computer constructions suggest $f(n)$ is much larger: a valid sequence of 26813 terms exists in $[1, 2\cdot10^7]$.