Does there exist a function F:C→C that is complex differentiable everywhere, maps every real number to a real number, is not equal on R to any affine map x mapsto ax+b, and preserves rationality in both directions; that is, for every x∈R, x∈Q if and only if F(x)∈Q?

Erdős Problem #226 — Entire Functions Preserving Rationality

This is Erdős Problem $226$ , asking whether an entire function can preserve rationality in both directions on the real line while being nonlinear. Barth and Schneider proved a stronger theorem in 1970, constructing entire functions that map arbitrary countable dense subsets of the reals onto one another monotonically.

Known results

Barth and Schneider, 1970: entire functions can map countable dense subsets of the reals onto one another monotonically, which yields the rationality-preserving example.
The formalized target asserts an entire complex function, real-valued on the real axis, that is not affine and satisfies $x\in\mathbb{Q}\iff f(x)\in\mathbb{Q}$ for every real $x$ .

AI-assisted formalization (date not stated)

A Lean development reports that ChatGPT selected and explained the classical proof, while Aristotle auto-formalized it; the resulting proof is claimed to verify in Lean. This is formal verification of an established result, not a new mathematical resolution.

Current status (as of March 2026): The problem is settled by Barth and Schneider's 1970 theorem; no mathematical issue remains open.

Erdős Problem #226 — Entire Functions Preserving Rationality

Primary source

Additional references

Progress summary

Solutions 0