we-solve (beta)

CS-112 · computer science · mathematics · Computational algebra and number theory · Logic and computability

Decidability of Rational Points over Number Fields

Status Open · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
$\mathbb N$, $\mathbb Z$, $\mathbb Q$, $\mathbb R$, and $\mathbb C$ denote the natural numbers, integers, rationals, reals, and complex numbers, respectively. All additional parameters and hypotheses are specified in the question.
Statement recorded in the supplied source.
Given a variety $X$ over a number field $k$, is there an algorithm that decides whether $X$ has a $k$-rational point?

Formulation references: [S1], [S2].

Short English statement

Given a variety $X$ over a number field $k$, is there an algorithm that decides whether $X$ has a $k$-rational point?

Sources

Catalogue entry

Statement licence: CC-BY-SA-4.0 · Source file

Contributions 1

CS-112-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for CS-112

The claimed undecidability over $\mathbb Q$ rules out a general algorithm for rational-point existence over number fields: an integer polynomial $f$ is sent to its affine zero locus $V(f)$ over $\mathbb Q$, whose rational points are exactly the rational solutions of $f=0$. The result already obstructs the requested procedure at $k=\mathbb Q$; it does not assert undecidability separately for each other fixed number field.

Decidability of Rational Points over Number Fields

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 004; 2026-09-24), the asserted result is that rational solvability of integer-coefficient polynomials with an unrestricted number of variables is undecidable.

Mathematical statement of the claimed result

Manuscript 1.
With $n$ variable and integral polynomial coefficients explicitly encoded, the rational Diophantine decision claim is \[ \{f\in\mathbb Z[X_1,\ldots,X_n]:\exists x\in\mathbb Q^n,\ f(x)=0\} \quad\text{is undecidable}. \] There is no algorithm giving the correct yes/no answer for every such input; the coefficient ring is $\mathbb Z$, but sought solutions lie in $\mathbb Q$.

Outline of the argument

For manuscript 1 (family 004; 2026-09-24), integer solvability is represented by an effective sequence of finite rational tests. Elliptic indices, odd valuation contacts, and a height argument force an ordinary integer witness when every test succeeds; a hypothetical rational decision procedure would then decide the integer problem by two concurrent searches.

Formal verification

No Lean formalization is listed at this snapshot for manuscript 1 (family 004; 2026-09-24).

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

Go to contribution →