---

Claim. Let $B$ be the supremum, over transcendental entire functions $f$, of $\liminf_{r\to\infty}\mu(r,f)/M(r,f)$, where $\mu(r,f)$ is the maximum term of the power series of $f$ at radius $r$ and $M(r,f)$ its maximum modulus there; $B$ is the value Problem 513 asks for. The record claims two things. First, $B\ge0.5850788196$, certified for an explicitly specified function of the two-parameter family of He and Tang, with the parameters the record names as $K=3.5682353$ and $\alpha=3.9615395411$ and found by the author's own search, through a dyadic root-cover certificate in 50-digit interval arithmetic that replays in about twelve seconds. The analytic step that turns the certified unit-circle maximum into a bound on $B$ is Theorem 2.8 of He and Tang's paper, whose card is he_2026_generalizing_clunie_hayman_construction_erdos_maximum. Second, an independent re-verification of the stronger bound $B\ge0.585078819653$ of Sothanaphan's note of 27 February 2026, which the record describes as AI-generated: a re-implementation from the mathematics with matching node counts, a reproduction of the public code with a defect in a library version patched, and a cross-check by a mesh and Lipschitz bound. The record puts its own bound about $8\times10^{-12}$ below that frontier, a gap that the ten digits its summary prints do not show and that rests on the further digits of its certified value; it leaves the upper bound $B\le2/\pi-c$ of Clunie and Hayman untouched. This account follows the tab entry's summary and notes and the record's description.

Submission note. Posted to erdosproblems.com as a proof claim by T. Alexander Lystad (account alexander_lystad) on 2 August 2026, giving "Kimi K3" as the AI used:

New certified lower bounds on B = sup_f liminf μ(r,f)/M(r,f). (1) We certify B ≥ 0.5850788196 from a fully specified He–Tang-family function (K = 3.5682353, α = 3.9615395411, our own search): a slack-free dyadic root-cover certificate in 50-digit interval arithmetic, ~12 s replay — the second-strongest certified bound, 8×10⁻¹² below the frontier, a certified pure construction gap. (2) Independent verification of the frontier B ≥ 0.585078819653 (Sothanaphan, 2026-02-27, AI-generated): from-the-math re-implementation (identical 3519/96 node counts), reproduction of the public code (mpmath ≥ 1.4 defect patched), and a method-independent mesh+Lipschitz cross-check. The Clunie–Hayman upper bound 2/π − c is untouched. Notes: Verification tier: exact interval-arithmetic certificates (mpmath.iv, 50 dps) — not Lean, not expert-verified. Replay from the writeup record: 'python root_cover_certificate.py --preset r9_own' (~12 s, VERDICT: PASS; regression presets ht_published, sothanaphan included); full logs ship in the record. Analytic step: He–Tang Thm 2.8 (arXiv:2602.12217). The page's displayed 0.5850788 is a truncation of the verified frontier. Production chain: AI-assisted search and code; all bounds machine-checked; human-prepared exposition.

Covers. A lower bound on $B$ only: $B\ge0.5850788196$ by the record's own certificate, and the earlier bound $B\ge0.585078819653$ re-verified. The value of $B$, and the upper bound, are not addressed, and the record does not move the lower frontier of Sothanaphan's note.

Standing. The claim was filed on the site's proof-claims tab on 2 August 2026 by the user alexander_lystad as a partial proof, with the claimant T. Alexander Lystad and an AI system named as Kimi K3; the notes describe the production as AI-assisted search and code with all bounds machine-checked and a human-prepared exposition, and say that the certificates are interval arithmetic, not Lean and not expert-verified. The site's label is OPEN and its page was last edited on 2 April 2026, before the claim; its commentary does not mention the record, and the tab entry has no comments. No refereed publication, no formalization and no outside review was found. The claim stays claimed.

Depends on. [[problems/analysis/E0513/claims/2026_02_12_he_tang|He and Tang's certified lower bound]], whose paper supplies the reduction of the limit inferior to the unit-circle maximum (their Theorem 2.8) and is unrefereed; the certificate is the record's own.