Conjectures.io

Number theory

Erdős 357 - monotone parts i

Let h(n)h(n) be the maximal kk such that there exist integers 1≤a1≤…≤ak≤n1 \le a_1 \leq \dotsc \leq a_k \le n such that all sums of the shape ∑u≤i≤vai\sum_{u \le i \le v} a_i are distinct. Is h(n)=o(n)h(n)=o(n)?

References

No one has attempted this yet.

Formal statement

Lean type

(fun n => ↑(Erdos357.h n)) =o[Filter.atTop] fun n => ↑n

What you must prove

import FormalConjectures.ErdosProblems.«357»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos357.erdos_357.variants.monotone.parts.i" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/357.lean

Source type SHA-256
sha256:512842f4dbee15ee80295d6e99985faef1dfb124f513c32389803c5d5a54a66a
Task id
fc-379fc029-parts-i-9f01a09d43-formalized-v1
Task commitment
sha256:00666e1c766ea2a8e9307e9120b67376d84fc5aabeac246b6d856928af540cbe

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.