Erdős problem 907

Let $f:\mathbb{R}\to \mathbb{R}$ be such that $f(x+h)-f(x)$ is continuous for every $h>0$ . Is it true that $f=g+h$ for some continuous $g$ and additive $h$ (i.e. $h(x+y)=h(x)+h(y)$ )?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

907.lean

Retained formal statement1 of 1

Let $f:\mathbb{R}\to \mathbb{R}$ be such that $f(x+h)-f(x)$ is continuous for every $h>0$ . Is it true that $f=g+h$ for some continuous $g$ and additive $h$ (i.e. $h(x+y)=h(x)+h(y)$ )?

A conjecture of Erdős from the early 1950s. Answered in the affirmative by de Bruijn [dB51].

FormalConjectures/ErdosProblems/907.leanErdos907.erdos_9074 linesExact file

1True ↔2  ∀ (f : ℝ → ℝ),3    (∀ (h : ℝ), 0 < h → Continuous fun x => f (x + h) - f x) →4      ∃ g a, Continuous g ∧ (∀ (x y : ℝ), a (x + y) = a x + a y) ∧ f = g + a

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.