Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. Let be such that, for every real , the function is continuous. Then for a continuous and an additive , that is, for all real . 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 only; since , 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 whose positive-shift differences are
continuous, the existence of a continuous and an additive with
for all . 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.