Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Konieczny proves, as Proposition 1.1, that for every some permutation of has at least distinct consecutive sums. The permutation is , that is for odd and for even . A consecutive sum of odd length equals with the entry at one end of the block, and this pair determines the block, so the odd-length sums are pairwise distinct; there are of them. Since is not , the question of Problem 34 has a negative answer. The paper also shows (Theorem 1.2) that the maximum of over lies between and , that a uniformly random permutation has in probability (Theorem 1.3), and that every permutation has (Proposition 6.1); its Section 1.5 draws the earlier counterexample with sums from Hegyvári's theorem, recorded on Hegyvári's page.
The paper's library card is [[../library/integer_sequences/konieczny_2015_consecutive_sums_permutations/_index|Konieczny 2015]], which records its arXiv v5 and journal versions (read, not held), with compiled pages for [[../library/integer_sequences/konieczny_2015_consecutive_sums_permutations/proposition_1_1|Proposition 1.1]], Theorems 1.2 and 1.3 and Proposition 6.1; the statements were checked and the half-page proof of the proposition read for structure, and nothing here is independently reviewed.
Formalization. The statement file of the formal-conjectures project
(FormalConjectures/ErdosProblems/34.lean) marks the problem solved and points,
through its formal_proof attribute, at a Lean 4 file in Boris Alexeev's
lean-proofs repository, linked above at a pinned commit. That file declares
itself a formalization of a solution to Problem 34, names N. Hegyvári and J.
Konieczny as its informal authors and Aristotle and Boris Alexeev as its formal
authors, and reproduces the prompt it was proved from: the permutation
, the distinctness of its odd-length consecutive sums, the
bound and the corollary that some permutation has at least
distinct consecutive sums. It is therefore recorded here as a formalization of
this claim, not as an independent result. Its theorem not_erdos_34 negates a
statement textually matching the collection's; the file contains no sorry and
no axiom command at the pinned commit. This project has not built the file or
audited its statement against the problem, so it supplies no formalized
evidence; the site's label DISPROVED (LEAN) refers to this development.
Acceptance. The paper is refereed: J. Konieczny, On consecutive sums in permutations, J. Combinatorics 12, no. 3 (2021), 413--477; the statements cited here agree word for word with the arXiv text. The site's curator, Thomas F. Bloom, marks Problem 34 disproved and credits this paper with the explicit permutation and the random-permutation asymptotic. The page is dated by the arXiv posting of 27 April 2015.