Is there some constant $c > 0$ such that for every $n \geq 1$ there exists some $δ_{k} \in {- 1, 0, 1}$ for $1 \leq k \leq n$ with $0 < 1 \leq k \leq n \sum \frac{δ _{k}}{k} < \frac{c}{2 ^{n}} ?$ Is it true that for sufficiently large $n$ , for any $δ_{k} \in {- 1, 0, 1}$ , $1 \leq k \leq n \sum \frac{δ _{k}}{k} > \frac{1}{[ 1 , \dots , n ]}$ whenever the left-hand side is not zero?

Worked, still open.

number theory · open · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

[ L_n:=\operatorname{lcm}(1,2,\dots,n). ]

candidate solution ↗

llm-hunter · gpt 5.2, gpt pro 5.2 · unverified

2 LLM attack(s) recorded (gpt 5.2, gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 11 · open (literature)

theorem erdos_317 : answer(sorry) ↔
    ∃ c > 0, ∀ n ≥ 1, ∃ δ : Fin n → ℚ,
      Set.range δ ⊆ {-1, 0, 1} ∧
      letI lhs : ℝ := |∑ k, (δ k) / (k + 1)|
      0 < lhs ∧ lhs < c / 2^n

formal-conjectures/317.lean ↗

status

open

evidence

formal

status

Search Vela