Number theory

Erdős problem 317 - claim 2

Is it true that for sufficiently large

n

, for any

\delta_k\in \{-1,0,1\}

\left\lvert \sum_{1\leq k\leq n}\frac{\delta_k}{k}\right\rvert > \frac{1}{[1,\ldots,n]}

whenever the left-hand side is not zero?

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Formal statement

Proof target

import FormalConjectures.ErdosProblems.«317»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos317.erdos_317.variants.claim2" := by
  sorry

end Bounty

Open this target’s Challenge.lean

Original conjecture (Lean type)

True ↔
  ∀ᶠ (n : ℕ) in Filter.atTop,
    ∀ (δ : Fin n → ℚ),
      δ '' Set.univ ⊆ {-1, 0, 1} → |∑ k, δ k / (↑↑k + 1)| ≠ 0 → |∑ k, δ k / (↑↑k + 1)| > 1 / ↑((Finset.Icc 1 n).lcm id)

Original conjecture source: FormalConjectures/ErdosProblems/317.lean

Source type SHA-256: sha256:63e6a8eb86ef9f7e24f6ca82d49befe2da0fb47d0ef92902d9d1a9e12117ddb0
Task id: fc-v2-variants-claim2-c6aebd21b6cc2360bc0d5249-formalized
Task commitment: sha256:3577736f5da40a56be2d9b9a1e3224a9448ecc7994ee351c8a27362ef8be8457

References

erdosproblems.com/317

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.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Join Bittensor Discord

Erdős problem 317 - claim 2

Is it true that for sufficiently large

n

, for any

\delta_k\in \{-1,0,1\}

\left\lvert \sum_{1\leq k\leq n}\frac{\delta_k}{k}\right\rvert > \frac{1}{[1,\ldots,n]}

whenever the left-hand side is not zero?

True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (δ : Fin n → ℚ), δ '' Set.univ ⊆ {-1, 0, 1} → |∑ k, δ k / (↑↑k + 1)| ≠ 0 → |∑ k, δ k / (↑↑k + 1)| > 1 / ↑((Finset.Icc 1 n).lcm id)