Conjectures.io

Number theory

Erdős 357 - part i

Let f(n)f(n) be the maximal kk such that there exist integers 1≤a1<…<ak≤n1 \le a_1 < \dotsc < 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 f(n)=o(n)f(n)=o(n)?

References

No one has attempted this yet.

Formal statement

Lean type

(fun n => ↑(Erdos357.f 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.parts.i" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/357.lean

Source type SHA-256
sha256:dfca10c65aedf442068a049d51581b0b7cb23c213aad3c2142bf1d0192826ca0
Task id
fc-379fc029-parts-i-e2813839bb-formalized-v1
Task commitment
sha256:a5ab8d0fbb646cc40abddd0bc82dd2c42d2a87ef4a75e5026abf7d6b3edb8e7e

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.