Skip to content

Questions with no algorithm (Hilbert's tenth problem)

Some requests look like ordinary computations but have no procedure that always finishes with the right answer. "Does this polynomial equation have a solution in fractions?" is one: a service that tries to answer it in general starts a search that, on some inputs, never ends, holding a worker until a timeout fires and the client retries. This page explains what is known about that question — Hilbert's tenth problem, over the integers and over the rationals, catalog result 004 — and why the library's router refuses it immediately instead of trying.

It assumes you know what a polynomial is. The router and its difficulty tags ("envelopes") are explained in Using the router; refusals in general in Refusals.

The situation

A computer-algebra endpoint, a notebook "solve over \(\mathbb Q\)" button, or a design check asks: given a polynomial with integer coefficients in several variables, such as \(x^3 + y^3 - 3xyz - 1\), is there a choice of rational numbers (fractions) for the variables that makes it zero? A complete answer means: for every input, the service eventually says yes or no, and is right.

The question this page answers is: can any program give that complete answer? If not, the honest product behaviour is a fast, explained refusal, with incomplete tools offered separately and labelled as incomplete.

Intuition: searching can confirm "yes" but never "no"

For any polynomial you can list all rational candidates in order of size and test each. If a solution exists, the search finds it eventually. If none exists, the search runs forever and never learns that it should stop. A complete procedure needs a way to say "no" in finite time. For integer solutions it has been proved that no such way exists in general. For rational solutions nobody knows.

The example's polynomial makes the point: \(x = 1, y = 0\) (any \(z\)) is a rational zero, so a search would succeed here. The refusal is not about this input; it is about promising an answer for every input.

Worked example: an optimistic request

Run:

uv run grounded-decision examples hilbert_refuse

The client asks for the rational zeros of \(x^3 + y^3 - 3xyz - 1\) and tags the request p_exact ("solvable exactly in polynomial time"). The router ignores the optimistic tag and answers at once:

OUTPUT ok=False  envelope=undec
       no complete algorithm for integer polynomials over Q (catalog 004)
       lean=False (a catalog/paper reference, not a Lean kernel check)

The same call in code:

from grounded_decision import Envelope, Subgoal, dispatch

r = dispatch(
    Subgoal("rational_zeros", Envelope.P_EXACT, {"poly": "x^3 + y^3 - 3xyz - 1"})
)
print(r.ok, r.envelope, r.detail)
# False undec no complete algorithm for integer polynomials over Q (catalog 004)

The polynomial string is never parsed, no search starts, and the result's value is the catalog reference for result 004.

The precise statement

Over the integers (theorem). There is no algorithm that, given a polynomial \(f \in \mathbb Z[x_1, \dots, x_n]\) (any \(n\)), decides whether \(f(x) = 0\) for some \(x \in \mathbb Z^n\). This is the negative answer to Hilbert's tenth problem (Matiyasevich, 1970, completing work of Davis, Putnam and Robinson): every set a program can list is the set of parameter values for which some polynomial equation has integer solutions, so deciding solvability would decide the halting problem.

Over the rationals (open). The same question with \(x \in \mathbb Q^n\) is open. The integer result would transfer if the integers could be described inside the rationals by a polynomial equation (if \(\mathbb Z\) were "Diophantine over \(\mathbb Q\)"); that is not known, and a conjecture of Mazur would rule it out. Related facts that are known: the full first-order theory of \(\mathbb Q\) is undecidable (Julia Robinson, 1949), and \(\mathbb Z\) has a definition in \(\mathbb Q\) using only universal quantifiers (Koenigsmann, 2016).

Special cases that are decidable. One variable: the rational root theorem lists finitely many candidates. A single quadratic equation: the Hasse–Minkowski theorem gives a procedure. Curves of genus 0 are also handled; for curves of genus 1 (elliptic curves) no algorithm is known to always work.

Where this result stands

In the wider literature: undecidable over the integers (theorem, Matiyasevich 1970). Over the rationals: open.

In this project's math catalog (result 004): no algorithm decides rational solvability of integer polynomials, that is, a negative answer over \(\mathbb Q\). Manuscript only: the catalog reference has lean=False, and the library's records say so.

What this library relies on: nothing. The refusal does not depend on the catalog claim being true. Even if a complete algorithm existed, its running time would be unbounded on some inputs, which has no place in a request path. See Where each result stands.

What the code does

dispatch(subgoal) in grounded_decision/router/dispatch.py refuses in two independent places:

  1. Any request tagged UNDEC (or EXPTIME_TRAP) is refused before its handler is looked up, with detail envelope UNDEC: refuse and no value. This applies to every subgoal name, not only this one.
  2. The rational_zeros handler refuses whatever tag it arrives with (p_exact, ugc_opt; fpras is refused before any handler), returning ok=False, envelope undec, the detail no complete algorithm for integer polynomials over Q (catalog 004) and the catalog reference as value.

There is no path that searches. The router does not distinguish one-variable or quadratic inputs, where a complete procedure exists; it refuses those too.

Limits, and what to do about them

  • The refusal is the product. Return it to the caller quickly (the example suggests HTTP 422 with the detail) instead of starting a worker.
  • Offer incomplete tools separately, and label them. For one variable, use the rational root theorem; that is complete. For several variables, offer a search over rationals up to a stated height (size of numerator and denominator) with a time limit, and report "no solution up to height \(H\)", never "no solution".
  • Do not cite the refusal as proof of impossibility. Over the rationals the impossibility is a catalog claim on an open problem. The reason to refuse in a service — unbounded running time — holds either way.
  • The tag is not checked against the input. A caller who tags a decidable request UNDEC gets a refusal too. Tag requests by the question asked, not by how hard you hope it is.