Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Problem 907
claims/: The 1 claim page of Problem 907, one per claimant's result; the problem's standing derives from them.
Statement. Let be such that is continuous for every . Is it true that
for some continuous and additive (i.e. )?
Status. The site labels the problem PROVED (LEAN), and its commentary
credits de Bruijn's 1951 theorem for the affirmative answer; the
formal-conjectures statement file's formal_proof attribute points to a Lean
proof of the statement in Alexeev's repository. Both are on the
claim page. The Lean
proof is not built here.
Source. erdosproblems.com/907, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #907, https://www.erdosproblems.com/907.
References.
- [dB51] de Bruijn, N. G., Functions whose differences belong to a given class. Nieuw Arch. Wiskunde (2) 23 (1951), 194-218.
Formalization. Statement in
formal-conjectures,
whose formal_proof attribute at the pinned commit points to the proof in
Alexeev's lean-proofs repository linked from the claim page; neither is built
or audited here.
Progress
Not yet compiled.
Known Results
Not yet compiled.
Linked library material
These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.