Erdős problem 226

Is there an entire non-linear function $f$ such that, for all $x\in\mathbb{R}$ , $x$ is rational if and only if $f(x)$ is?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

226.lean

Retained formal statement1 of 1

Is there an entire non-linear function $f$ such that, for all $x\in\mathbb{R}$ , $x$ is rational if and only if $f(x)$ is?

Barth and Schneider [BaSc70] proved the stronger result for countable dense subsets of $\mathbb{R}$ .

FormalConjectures/ErdosProblems/226.leanErdos226.erdos_2265 linesExact file

1True ↔2  ∃ F,3    Differentiable ℂ F ∧4      (∀ (x : ℝ), (F ↑x).im = 0) ∧5        (∀ (g : ℝ →ᵃ[ℝ] ℝ), (fun x => (F ↑x).re) ≠ ⇑g) ∧ Erdos226.PreservesRationality fun x => (F ↑x).re

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.