---

Claim. The answer is no: for $f(z)=z^{16}-1$, the projection of $\{z:|f(z)|\le1\}$ onto every line through the origin has measure greater than $2$. The Lean development Erdos1043 in Boris Alexeev's repository proves the negated form of the formal-conjectures statement from this one polynomial, as erdos_1043 in the file first posted for Lean v4.24.0 and as not_erdos_1043 in the revision of 2026-09-15 linked above; its level set is a sixteen-petaled lemniscate, and the proof turns on the inequality $2^{1/16}\cos(\pi/16)>1$, as the author's thread post of 2025-12-28 says and the file's lemma inequality states. The posted file's header says that the proof was found by Aristotle, the system of Harmonic, from the formal statement alone, and credits the original disproof to Pommerenke's 1961 paper. The construction is not Pommerenke's (his is the five-armed star of capacity $1$ with every projection above $2.386$), so the proof is recorded as its own claim beside Pommerenke's accepted page rather than as a formalization of it. A later thread post observes that $z^3-1$ is already a counterexample; it is a remark, not a dated manuscript, and gets no page.

Second development. A second Lean proof of the same statement by the same polynomial, by the GitHub user XC0R, is kept in that user's fork of formal-conjectures and is the second formalization link above. Its pull request, merged on 13 April 2026, attributes the counterexample $z^{16}-1$ to Pommerenke, whose construction it is not, proves the measure bound through star-convexity of the level set about the origin, the symmetry $(-z)^{16}=z^{16}$ and the same inequality $2^{1/16}\cos(\pi/16)>1$, and says that it was assisted by Claude (Anthropic) for the Lean translation. The formal-conjectures attribute points to a commit of the fork that no longer resolves; the link above is the pull request's first commit, which holds the complete proof that the merged head later removed. Its lemmas follow Alexeev's file by name, and its proof of inequality is Alexeev's, so it is recorded here as a translation of this claim's development rather than as its own claim.

Acceptance. Formalized. This corpus's verification built Alexeev's lean-proofs repository at the pinned commit 8822f7dd of 2026-09-15, in its src/latest folder (Lean v4.33.0, Mathlib v4.33.0), and checked the axioms of Erdos1043.not_erdos_1043, which are exactly propext, Classical.choice and Quot.sound. The folder's comparator challenge for the problem pins that theorem together with the definition Erdos1043.levelSet and the local instance Erdos1043.instMeasureSpaceRealSpan that its type reaches, and the theorem's fingerprint was found identical to the challenge's; the two statements are textually identical, and the solution uses no sorry, added axiom or native_decide. The statement was audited clause by clause against the problem's Statement: a monic non-constant polynomial is a monic polynomial of degree at least $1$; lines through the origin suffice, since projections onto parallel lines are translates of equal length; the local instance makes the volume on the line its length; and the theorem asserts that some such polynomial has, for every unit vector, a projection of $\{|f|\le1\}$ onto the line it spans of measure greater than $2$, which is the negative answer. The witness $z^{16}-1$ is fixed in the proof, not in the statement. What was built is that later revision, not the file first posted for Lean v4.24.0: the author reports the posted development as verified in their repository (Lean toolchain v4.24.0, Mathlib v4.24.0), and their thread post links an online type-check of it at Mathlib v4.24.0 (live.lean-lang.org). The formal-conjectures statement file for the problem, at its revision of 2026-09-18 (1043.lean), tags the problem research solved and lists this development first under its formal_proof attribute, with XC0R's proof second, and the Lean qualifier of the site's label refers to it. Not reviewed: no outside reviewer of the proof is named. Not refereed: the result is a Lean development with no journal publication.

Depends on. Nothing on the wiki; the development imports only Mathlib.