Skip to content

Erdős problem 226

Start work

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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/226.lean

Formal Conjectures

FormalConjectures/ErdosProblems/226.leanErdos226.erdos_2265 linesExact file
True ↔  ∃ F,    Differentiable ℂ F ∧      (∀ (x : ℝ), (F ↑x).im = 0) ∧        (∀ (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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:226
  • PLBY Lean proofsErdosProblems.Erdos226

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry