---

Claim. For every monic cubic $p\in\mathbb{C}[z]$ the length of the lemniscate $\{z:\lvert p(z)\rvert=1\}$ is at most that of $z^3-1$, with equality only when $p$ is $z^3-1$ up to rotation and translation. This is the degree-3 case of the question of Problem 114, the conjecture of Erdős, Herzog and Piranian, and it is asserted conditionally: the write-up and its Lean development take as a cited hypothesis a domain reduction attributed to Eremenko and Hayman and to Proposition 1.2 of Tao 2025, by which a maximizer is connected and has its critical points on the lemniscate, so that the question is reduced to a one-parameter family of cubics in a real normal form. The author presents that hypothesis as a published theorem rather than a conjecture, so the claim is recorded as a partial claim (degree 3) with the cited hypothesis stated here, not as a conditional one; the cited results do not give the reduction the Lean structure declares, as the Lean paragraph below records. The author, Bertrand Chatelet, posted the write-up Erdős–Herzog–Piranian conjecture — proof for d=3 and the Lean sources to the repository linked above on 2026-08-22, deposited the write-up on Zenodo on 2026-08-24, and registered the claim on the site's proof-claims page on 2026-09-07 as a partial claim, noting there that an earlier submission appeared to have been removed. The author's own description says that the text is a demonstrative write-up of the analytic chain for that family and not an unconditional, self-contained proof for every monic cubic.

Submission note. Posted to erdosproblems.com as a proof claim by b chatelet (account bchatelet) on 7 September 2026:

This text is a demonstrative write-up of a retained analytic chain for the critical-onfamily in degree , conditional on a domain reduction cited from the literature (Part I: Eremenko–Hayman; Tao, Prop. 1.2, arXiv:2512.12455). It is not an unconditional, self-contained proof of EHP for every monic cubic from first principles. Notes: I don’t know whether my previous submission was registered, as it seems to have been deleted without any comment. Therefore, I am submitting it again.

Covers. Monic polynomials of degree 3 only, resting on the domain reduction the write-up cites from Eremenko–Hayman and Tao. The Lean theorem at the pinned commit covers less than the write-up asserts: its cubics have real coefficients only, and its hypothesis is a length identity over every real monic cubic that the cited results do not give and that fails, so the formal theorem is vacuous (the Lean paragraph below). The degree-2 case was proved by Eremenko and Hayman (Eremenko–Hayman 1999) and the case of all sufficiently large degree is claimed, pending, by Tao (Tao 2025), with $z^n-1$ the unique maximizer up to rotation and translation; the remaining degrees, which Tao's Remark 1.3 says are finitely many and effectively bounded, are not touched by this claim beyond $n=3$. Dahlke's manuscript of 2026-05-20 (Dahlke 2026) claimed the degree-3 inequality, without a uniqueness clause, three months before this write-up.

Argument, as the write-up states it. Parts II to VII bound the length of the lemniscate of a cubic in the reduced family by splitting the defect against $z^3-1$ into zones, bounding each by explicit quadratures (two of them in closed form) and rational constants, and closing the comparison on two ranges of the family's parameter by two routes, one of them a chord bound. Python scripts in an appendix are floating-point checks outside the logical chain.

Lean development. The folder EhpD3/lean_ehp_d3 of the repository, at the pinned commit of 2026-08-24, builds the library LeanEhpD3, whose root imports LeanEhpD3/Conjecture.lean. That file declares the hypothesis as a structure DomainReductionD3 with three fields: a map reduce from monic cubics to the real normal form RealNorm (the cited reduction), an identity length_eq stating that every monic cubic has the lemniscate length of its reduction, and a window window stating that the reduction's parameter $\varepsilon$ is at most $1/2$. Its theorem ehp_d3 takes a value of that structure and a monic cubic and concludes that the length is at most that of $z^3-1$, and strictly less when the reduction's parameter $\kappa$ is positive; it goes through ehp_d3_family_length, which splits the family into the range $\varepsilon\le1/5$ (master_gap) and the range from $1/5$ to $1/2$ (master_gap_route2), so both routes are in Lean. The window of at most $1/5$ and the note that widening it and wiring the second route into ehp_d3 remained to be done survive only in a root-level Conjecture.lean outside the library and in the Zenodo description, which reports the state of 2026-08-22; the repository's README of 2026-08-24 marks the second route done and reports a green build with no sorry or admit. Three features of the formal statement bear on what it proves. First, MonicCubic has real fields $a,b,c$, so ehp_d3 covers real-coefficient cubics only and not the complex cubics the problem asks about. Second, length_eq quantifies over every cubic and requires each real monic cubic to have the lemniscate length of a member of the normal-form family $z^3+3k^{2/3}z-\sqrt{1-4k^2}$, $k\in[0,1/2]$, whose members have connected lemniscates through their critical points; the cited reduction is weaker, since Proposition 1.2 of Tao, from Lemmas 5 and 6 of Eremenko–Hayman, gives one maximizer with those properties and says nothing about other cubics. Third, the identity fails: the lemniscate of $z^3-27$ is three small ovals of total length about $2\pi/9$, far shorter than the connected lemniscate of any family member, so DomainReductionD3 has no value and ehp_d3 holds vacuously. The write-up's uniqueness clause likewise restates Proposition 1.2 as holding for any maximizer, while Tao proves only that one maximizer with those properties exists. This corpus has not built or audited the development; the link is a posting of the result and not formalized evidence, and the site's problem page records no attempt by anyone else to check it.

Depends on. No page of this wiki.

Acceptance. None recorded. The site's label is FALSIFIABLE (problem page last edited 2026-01-23), the proof-claims entry carries no comments and no acceptance mark, and the proof-claims thread, the Zenodo record and the repository record no review, referee report or acknowledgment by anyone outside the author. Proof coverage: none; the write-up's analytic chain is unverified in this corpus, and the Lean development is unbuilt and unaudited.