Skip to content

Erdős problem 1121

If C1,…,CnC_1,\ldots,C_n are circles in R2\mathbb{R}^2 with radii r1,…,rnr_1,\ldots,r_n such that no line disjoint from all the circles divides them into two non-empty sets then the circles can be covered by a circle of radius r=∑rir=\sum r_i.

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/1121.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1121.leanErdos1121.erdos_11217 linesExact file
∀ {n : ℕ} (c : Fin n → EuclideanSpace ℝ (Fin 2)) (r : Fin n → ℝ),  (∀ (i : Fin n), 0 < r i) →    (∀ (v : EuclideanSpace ℝ (Fin 2)) (t : ℝ),        v ≠ 0 →          (∀ (i : Fin n), ∀ p ∈ Metric.closedBall (c i) (r i), inner ℝ v p ≠ t) →            (∀ (i : Fin n), inner ℝ v (c i) < t) ∨ ∀ (i : Fin n), t < inner ℝ v (c i)) →      ∃ z, ⋃ i, Metric.closedBall (c i) (r i) ⊆ Metric.closedBall z (∑ i, r i)
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:1121
  • PLBY Lean proofsErdosProblems.Erdos1121

Reported activity

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

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page