Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated


Claim. Let f:R→Rf:\mathbb{R}\to\mathbb{R} be such that, for every real hh, the function x↦f(x+h)−f(x)x\mapsto f(x+h)-f(x) is continuous. Then f=g+Hf=g+H for a continuous gg and an additive HH, that is, H(x+y)=H(x)+H(y)H(x+y)=H(x)+H(y) for all real x,yx,y. This is Theorem 1.1 of de Bruijn's paper, where it is stated as a conjecture of Erdős, and it answers the question of Problem 907 in the affirmative. The problem assumes continuity of the differences for h>0h>0 only; since f(x−h)−f(x)=−(f((x−h)+h)−f(x−h))f(x-h)-f(x)=-\bigl(f((x-h)+h)-f(x-h)\bigr), the difference for a negative shift is the negative of a translate of a positive-shift difference and is continuous as well, so the hypothesis of the theorem follows from the problem's. The paper's digest is the [[../library/analysis/debruijn_1951_functions_whose_differences_belong_given_class/_index|source card]].

Acceptance. The result is refereed: N. G. de Bruijn, Functions whose differences belong to a given class, Nieuw Archief voor Wiskunde (2) 23 (1951), 194–218, received by the journal on 6 December 1950. It is reviewed in the sense of a documented independent acceptance: Thomas Bloom, the curator of erdosproblems.com, marks Problem 907 proved and credits de Bruijn's paper for the affirmative answer. Pietro Monticone posted a Lean 4 formalization on the site's discussion thread on 7 April 2026, as a gist whose header names de Bruijn as the informal author and Aristotle (from Harmonic) and Monticone as the formal authors, and which proves, for every ff whose positive-shift differences are continuous, the existence of a continuous gg and an additive HH with f(x)=g(x)+H(x)f(x)=g(x)+H(x) for all xx. Boris Alexeev's lean-proofs repository carries a modified copy, Erdos907.lean, whose header names the gist and that post as its sources, and the formal_proof attribute of the statement file in formal-conjectures points to that copy; the site's label is PROVED (LEAN). This corpus has not built or audited either file, so both are linked above and neither is listed as formalized evidence.

The page is dated to the year of publication; the journal volume prints no fuller date for the article.