Skip to content

Erdős problem 34

For any permutation π∈Sn\pi\in S_n of {1,…,n}\{1,\ldots,n\} let S(π)S(\pi) count the number of distinct consecutive sums, that is, sums of the shape ∑u≤i≤vπ(i)\sum_{u\leq i\leq v}\pi(i). Is it true that S(π)=o(n2) S(\pi) = o(n^2) for all π∈Sn\pi\in S_n?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

34.lean

Retained formal statement1 of 1

For any permutation π∈Sn\pi\in S_n of {1,…,n}\{1,\ldots,n\} let S(π)S(\pi) count the number of distinct consecutive sums, that is, sums of the shape ∑u≤i≤vπ(i)\sum_{u\leq i\leq v}\pi(i). Is it true that S(π)=o(n2) S(\pi) = o(n^2) for all π∈Sn\pi\in S_n?

Hegyvári [He86] gave a counterexample.

FormalConjectures/ErdosProblems/34.leanErdos34.erdos_341 lineExact file
False ↔ ∀ (c : ℝ), 0 < c → ∃ N, ∀ n ≥ N, ∀ (p : Equiv.Perm (Fin n)), ↑(Erdos34.consecutiveSums n p).card < c * ↑n ^ 2
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Search problems.science

Find a Problem, Result, source, or page