---

Claim. The statement of Problem 1126 holds: if $f(x+y)=f(x)+f(y)$ outside a null set of pairs $(x,y)\in\mathbb R^2$, there is an everywhere-additive $h$ with $f=h$ outside a null subset of $\mathbb R$. This is the theorem of Section 2 of N. G. de Bruijn, On almost additive functions, Colloquium Mathematicum 15 (1966), no. 1, 59–63; see its library card and the theorem's page. The proof takes, by Fubini's theorem, a null set $M$ outside of which the vertical sections of the exceptional set are null, shows that $f(x+y)-f(y)$ is almost everywhere constant in $y$, defines $h(x)$ as that constant, and proves additivity by choosing one pair $(w,z)$ outside five null sets. The paper also derives Hartman's earlier theorem for a fixed null set excluded from each input, abstracts the argument to thin and light subsets of abelian groups, and proves a quantitative form allowing an exceptional plane set of finite outer measure. The route differs from Jurkat's independent proof, which extends $f$ through consistent representations in a conull sumset.

Acceptance. Refereed: the paper appeared in Colloquium Mathematicum, received by the editors on 1 December 1964. Reviewed: Thomas Bloom, the curator of erdosproblems.com, labels the problem proved and credits it as proved independently by de Bruijn and Jurkat. The page is dated by the year of publication; the fascicle prints no fuller date. Jurkat's added-in-proof note records that the manuscript reached him in September 1964.

Formalization. The Lean 4 file Erdos1126.lean in Boris Alexeev's repository declares itself a formalization of de Bruijn's solution, naming de Bruijn as its informal author and Aristotle, the system of Harmonic, and the forum user JoshuaB as its formal authors; its comment says the proof follows de Bruijn's three steps, the null set $M$, the construction of $h$ from shifted values, and the additivity and agreement of $h$ with $f$. Its theorem erdos_1126 states the result above, and the link pins the commit that placed the file at that path. The site's label, "PROVED (LEAN)", refers to this proof. The corpus has not built or audited the file, so no formalized evidence is listed; the formal-conjectures statement file that points to it is a statement, not a formalization.

Depends on. Nothing in this wiki: the argument is the paper's own.