Erdős Problem #1043

GPT-5 found that the problem had already been solved in the literature (12 Oct 2025). 3 AI contributions are recorded in all.

Problem
Erdős problem #1043 (analysis); current status: disproved (Lean)
Credit
GPT-5 · Literature search
Checked
Lean formalizationListed in Tao's wiki
Timeline
First AI contribution 2025-10-12 · wiki data as of 2026-06-30
Sources
Problem page (erdosproblems.com)Tao's AI-contributions wiki
PRIOR
ARTPer Tao's AI-contributions wiki

The problem

Let f∈C[x]f\in \mathbb{C}[x] be a monic non-constant polynomial. Must there exist a straight line ℓ\ell such that the projection of

{z:∣f(z)∣≤1}\{ z: \lvert f(z)\rvert\leq 1\}

onto ℓ\ell has measure at most 22?

Statement quoted from erdosproblems.com/1043, maintained by Thomas Bloom. Original source: [EHP58]. Current status there: disproved (Lean).

AI contributions

As recorded in Terence Tao's wiki AI contributions to Erdős problems (data as of 30 Jun 2026). 🟢 full, 🟡 partial, ⚪ unverified, 🔴 incorrect.

Date Kind AI systems Outcome Literature
12 Oct, 2025 Literature search GPT-5 🟢 Full solution found —
28 Dec, 2025 AI building on known literature Aristotle 🟢 New proof found (Lean) 🟢 Pommerenke (1961)
30 Dec, 2025 AI building on known literature GPT 🟢 New proof found 🟢 Pommerenke (1961); Aristotle

Caveats

The wiki's classifications are provisional and are not a benchmark. Many Erdős problems have never had a thorough literature review, so a result that looks new may later turn out to be known; some problems were also stated ambiguously or incorrectly. See the problem page for the full discussion.

∎