---

Bálint [Ba60b] proves the conjecture of Erdős that his opening paragraph states: if $q(y)=\prod_{m=0}^n(y-a_m)$ has only real zeros, in arithmetic progression $a_m-a_{m-1}=d$, then the distances between consecutive zeros of $q'$ increase as one moves from the midpoint $(a_0+a_n)/2$ of the zeros toward either endpoint. This is the corrected Statement of Problem 1114, with degree $n+1$, zeros $a_0<\cdots<a_n$ and the interval $(a_0,a_n)$; the site's wording writes the degree as $n$ and the right endpoint as $a_m$, and the problem page's Notes record that defect. The affine change $y=a_0+dx$ reduces the claim to $p(x)=x(x-1)\cdots(x-n)$, whose derivative has one zero $t_k$ in each interval $(k-1,k)$, the zeros of $\sum_m1/(x-m)$. Two lemmas give the symmetry $t_k\mapsto n-t_k$ of these zeros about $n/2$ and a sign criterion for $\sum_m1/(x-m)$ on the intervals; the proof then compares $t_{k+1}$ with $t_k+1$ and closes by showing that the sum is negative at $(t_{k+1}+t_{k-1})/2$, which is $t_{k+1}-t_k>t_k-t_{k-1}$. The whole argument is elementary real analysis on the logarithmic derivative; the source card digests the paper, which is in Hungarian with an English summary. The paper prints no received date, so the page is dated by its publication year.

Depends on. Nothing in this wiki; the result rests on the published paper linked above.

Acceptance. Refereed: the paper appeared in Matematikai Lapok 11 (1960), 33–40; the paper link is the journal's scan in the REAL-J repository of the Hungarian Academy of Sciences. Reviewed: the site's curator, Thomas F. Bloom, labels the problem PROVED and credits Bálint in the problem's commentary (page last edited 2025-12-29), and Lorch's refereed paper of 1976 (card), Acta Math. Acad. Sci. Hungar. 27 (1976), 293–300, names the theorem the Erdős–Bálint result, restates it as the positivity of the second difference of the derivative's zeros, and builds its own monotonicity properties beside it. The theorem statement and the shape of the proof were checked against the paper; the proof is not compiled in this wiki. Formalization: a Lean 4 file in Boris Alexeev's lean-proofs repository, linked above at its pinned commit, declares itself a formalization of Bálint's solution, names Codex and GPT-5.6 Sol as its formal authors, and proves erdos_1114: for a nonzero real polynomial of degree $N+1$ vanishing at the $N+1$ points of an arithmetic progression, with one derivative zero in each gap, the gaps between consecutive derivative zeros are monotone outward on the right half and symmetric about the midpoint; its docstring notes that it proves the non-vacuous reading of the statement, with the degree one more than the site's index. The file ends with an axiom print. The corpus has not built or audited that development, so no formalized evidence is listed.