Mathoverflow 21003

Is there any polynomial $f(x, y) \in \mathbb{Q}[x, y]$ such that $f : \mathbb{Q} \times \mathbb{Q} \rightarrow \mathbb{Q}$ is a bijection?

Field theory and polynomials AMS 12

Mathematical statement

Is there any polynomial $f(x, y) \in \mathbb{Q}[x, y]$ such that $f : \mathbb{Q} \times \mathbb{Q} \rightarrow \mathbb{Q}$ is a bijection?

Statement source: MathOverflow statement material

Statement terms: CC-BY-SA-4.0

Attributed source material. Reuse must follow the linked attribution and share-alike terms.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

mathoverflow_21003

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem mathoverflow_21003 :    answer(sorry) ↔ ∃ f : MvPolynomial (Fin 2) ℚ, Function.Bijective fun x ↦ f.eval x := by  sorry

Statement source: Formal Conjectures
Lean version: v4.27.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Pinned Formal Conjectures sourceformalization mathoverflow/21003background *Z.H.*background