---

Claim. Theorem 1 of Gerald R. Mac Lane, On a conjecture of Erdös, Herzog, and Piranian, states: let $A$ be a compact subset of the open unit disc contained in a simply connected domain $\Delta$ with $0\notin\Delta\subset\{|z|<1\}$; then there is $n_0=n_0(A)$ such that for every $n\ge n_0$ some polynomial $P_n$ of degree $n$ has all its zeros on the unit circle, $P_n(0)=1$, and $|P_n(z)|>2$ for every $z\in A$. Such a $P_n$ belongs to the class of [[problems/analysis/E1215/_index|Problem 1215]], and every path from $0$ to the unit circle on which $|P_n|<1$ except at $0$ must avoid $A$. Mac Lane's Example 1 takes $A$ to be the spiral $z=\rho(1-e^{-t})e^{it}$, $2\pi\le t\le T$, with $0<\rho\le1$; a path from $0$ to the circle avoiding it has length greater than $\rho(1-e^{-2\pi})(T-4\pi)$, and $T$ is arbitrary. Hence the least constant $L_n$ that works for degree $n$ tends to infinity, and no constant $C$ works for every degree: the answer is no. His Examples 2 and 3 are a comb of alternating circular arcs and a two-arc labyrinth with radial walls, each showing that arbitrarily long stretches of any admissible path can be forced into an arbitrarily small neighborhood of $0$. Theorem 1 is deduced from Theorem A, a Jordan-curve approximation theorem taken from Mac Lane's 1949 Duke paper with one gap filled in the note: polynomials with all zeros on the boundary curve converging to $3$ on $\Delta$ and to $1$ near $0$, normalized by their value at $0$. Mac Lane's class allows $|P(0)|=1$, but the polynomials his theorem produces satisfy $P(0)=1$ exactly, so no normalization gap separates the paper from the problem. Cohen's 1952 note, that some path from $0$ to the circle on which $|P|<1$ everywhere except at $0$ always exists, and Loewner's polynomial whose modulus exceeds one at some point of every radius, recorded by Erdős, Herzog and Piranian in their 1955 paper (source card), are the context; that paper records Mac Lane's negative answer.

Acceptance. The paper is refereed: Michigan Math. J. 2 (1953/54), no. 2, 147–148, received by the editors on 16 October 1954 according to its first page. The site's key is Ma53, and the publisher's record gives the volume's two-year span and no month; the note cannot predate its receipt, so this page is dated by the receipt date, the earliest date the record prints. The site's curator, Thomas F. Bloom, marks Problem 1215 disproved and credits Mac Lane's theorem, the reviewed evidence. The three comments in the site's thread share pictures of Examples 2 and 3 and claim no result.

Formalization. Erdos1215.lean in Boris Alexeev's lean-proofs repository, pinned at the commit of 15 September 2026 in the link, declares itself a formalization of a solution to Problem 1215, names Mac Lane as its informal author and Codex and GPT-5.6 Sol as its formal authors, and is a link on this page, not a claim of its own. Its theorem not_erdos_1215 (line 132) states that no real constant $C$ works for every polynomial $P$ with $P(0)=1$, positive degree and all roots on the unit circle, where a path for $P$ is a continuous $\gamma$ on $[0,1]$ with $\gamma(0)=0$, $|\gamma(1)|=1$ and $|P(\gamma(t))|<1$ for $t\neq0$, and its length is the extended variation of $\gamma$ on $[0,1]$; the file derives it from hasArbitrarilyLongCounterexamples, a labyrinth of alternating walls on which a Mac Lane polynomial exceeds $2$ in modulus. At the pinned commit neither Erdos1215.lean (147 lines) nor the five companion modules it imports contain sorry; this corpus has not built or audited them, so no formalized evidence is listed. Formal-conjectures has no statement file for the problem.

Depends on. Nothing beyond the cited paper.