Skip to content

Erdős problem 498

Let z1,,znCz_1,\ldots,z_n\in\mathbb{C} with 1zi1\leq \lvert z_i\rvert for 1in1\leq i\leq n. Let DD be an arbitrary disc of radius 11. Is it true that the number of sums of the shape i=1nϵizi for ϵi{1,1}\sum_{i=1}^n\epsilon_iz_i \textrm{ for }\epsilon_i\in \{-1,1\} which lie in DD is at most (nn/2)\binom{n}{\lfloor n/2\rfloor}?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/498.lean

Formal Conjectures

FormalConjectures/ErdosProblems/498.leanErdos498.erdos_4985 linesExact file
True  ∀ (n : ℕ) (z : Fin n → ℂ),    (∀ (i : Fin n), 1 ≤ ‖z i‖) →      ∀ (c : ℂ),        {ε | (∀ (i : Fin n), ε i = -1 ∨ ε i = 1) ∧ ∑ i, ↑(ε i) * z iMetric.ball c 1}.ncardn.choose (n / 2)
SolvedStatement only, no proof

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:498
  • PLBY Lean proofsErdosProblems.Erdos498

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • Formalization

    Erdős AI contributions wiki · Jan 27, 2026

    Machine
    Aristotle, Claude Opus, Gemini Flash, Gemini Pro
    Open the source record

Continue

Search problems.science

Find a Problem, Result, source, or page