---

Claim. The statement of Problem 1121 is true. A. W. Goodman and R. E. Goodman, A circle covering theorem, Amer. Math. Monthly 52 (1945), no. 9, 494--498, prove that if closed disks $C_1,\ldots,C_n$ in the plane with radii $r_1,\ldots,r_n$ are nonseparable, that is, no line disjoint from every disk has disks on both of its sides, then a single disk of radius $r_1+\cdots+r_n$ contains them all. The paper reports the statement as a conjecture of Erdős.

Its statement and the attribution to Erdős are taken from the account in A. Akopyan, A. Balitskiy and M. Grigorev, On the circle covering theorem by A. W. Goodman and R. E. Goodman, Discrete Comput. Geom. 59 (2018), no. 4, 1001--1009 (arXiv:1605.04300), and from the site's page. That account describes Goodman and Goodman's proof as projecting the family onto orthogonal directions and applying the lemma for nonseparable segments on a line.

Depends on. No page of this wiki.

Acceptance. The result is refereed: it appeared in the American Mathematical Monthly. The site's curator, Thomas Bloom, marks the problem proved and credits Goodman and Goodman with the proof (problem page last edited 17 April 2026). Four later published proofs settle the same statement and have their own pages: Hadwiger's inequalities for nonseparable convex systems, which the curator records as a generalization rather than an independent proof, Bezdek and Litvak's analytic proof, Bezdek and Lángi's theorem for symmetric bodies and Akopyan, Balitskiy and Grigorev's theorem for arbitrary bodies.

Formalization. Boris Alexeev's lean-proofs repository holds, at the pinned commit linked above, a Lean 4 file whose header declares it a formalization of a solution to Problem 1121 with Goodman and Goodman as the informal authors and Aristotle (Harmonic) and Amogh Parab as the formal authors; Parab announced it on the site's discussion thread on 16 April 2026, and the site's label carries a Lean marker. Its theorem Erdos1121.erdos_1121 takes a family circles : Fin n → Circle2D of centers with positive radii in EuclideanSpace ℝ (Fin 2) and the hypothesis CirclesNonseparable circles, that no line at distance greater than the radius from every center has centers on both sides, and concludes that some point T has every closed ball of the family inside the closed ball about T of radius ∑ j, (circles j).radius; the file prints the axioms of that theorem as propext, Classical.choice and Quot.sound. This corpus has not built the file, audited its axioms or reviewed its statement, so the file is a link here and not formalized evidence.