Skip to content

Erdős problem 296

Start work

Let N≥1N\geq 1 and let k(N)k(N) be maximal such that there are kk disjoint A1,…,Ak⊆{1,…,N}A_1,\ldots,A_k\subseteq \{1,\ldots,N\} with ∑n∈Ai1n=1\sum_{n\in A_i}\frac{1}{n}=1 for all ii. Estimate k(N)k(N). Is it true that k(N)=o(log⁡N)k(N)=o(\log N)?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/296.lean

Formal Conjectures

FormalConjectures/ErdosProblems/296.leanErdos296.erdos_2962 linesExact file
(∀ (N k : ℕ), Erdos296.HasDisjointUnitDecomps N k → ↑k ≤ Erdos296.recipSum (Finset.Icc 1 N)) ∧  ∀ (ε : ℝ), 0 < ε → ε < 1 → ∀ᶠ (N : ℕ) in Filter.atTop, Erdos296.HasDisjointUnitDecomps N ⌊(1 - ε) * Real.log ↑N⌋₊
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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:296
  • PLBY Lean proofsErdosProblems.Erdos296

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry