Skip to content

A root is shown, an absence is proved

Vitaly Reznik

This page started from a remark I heard in an interview with Terence Tao on Lex Fridman's podcast, paraphrased here because I have no exact quote: whether some polynomial equations have solutions depends on the axioms you accept. Strictly, what depends on the axioms is whether a solution, or its absence, can be proved; whether one exists is a fact about the whole numbers. My first thought was that ZTL proves its theorems with none of Lean's standard axioms, so perhaps it escapes the problem. It does not, and the reason is worth writing down. What ZTL can do is name what each answer rests on.

On this page proved marks a theorem checked in Lean 4, a proof assistant in which a machine checks every step, using none of Lean's three standard axioms (Lean's own type theory remains, as the ground of any Lean proof). Measured marks an exact computation by a program you can run. Cited marks a known result that is not re-proved here. My reading marks what I take the results to mean. Open marks what is not settled.

Terms

  • A Diophantine equation asks for whole-number solutions of a polynomial equation, such as x² − 61y² = 1.
  • A witness is one particular solution. Substituting it checks it.
  • A search tries values up to some bound.
  • A proof shows a statement for all values at once.
  • A theory (such as ZFC, the usual axioms of set theory) is a fixed set of axioms and rules. It is consistent if it never proves a contradiction.

What is already known

  • Cited. Matiyasevich, building on Davis, Putnam and Robinson (1970): every listable set of numbers (one a program can list) is the set of values for which some polynomial equation has a whole-number solution. One consequence: for any theory whose theorems a program can list, there is a polynomial that has no root in the whole numbers exactly when that theory is consistent.
  • Cited. Gödel's second incompleteness theorem: a consistent theory of that kind that contains enough arithmetic does not prove its own consistency. So it does not prove that this polynomial has no root, and if the theory is consistent, the polynomial really has none.
  • Writing such a polynomial down explicitly is hard. Known constructions go through a universal Turing machine (J. P. Jones, "Universal Diophantine equation", Journal of Symbolic Logic 47, 1982) or a formula for provability, and the results are far too large to search by hand.

A root is shown: Pell's equation

Measured (dilemmas/diophantine.py): x² − 61y² = 1 has the trivial root x = 1, y = 0, and no other root with y between 1 and a million. Someone who searched that far and concluded "there is no other root" would be wrong: the smallest one lies more than two hundred times further. The continued fraction of √61 gives it:

x = 1 766 319 049,   y = 226 153 980

Proved: 1766319049 · 1766319049 = 61 · 226153980 · 226153980 + 1 (ZDiophantine.pell61_witness). The machine multiplies the numbers out.

An absence is proved: x² = 3y + 2

Proved: for all whole numbers x and y, x · x ≠ 3 · y + 2 (ZDiophantine.no_root_three). A square leaves remainder 0 or 1 when divided by 3, and 3y + 2 leaves remainder 2. No search through the numbers, however long, covers every x. The proof does: it reduces the question to three cases, one per remainder, a finite check. (The remainder function is defined and reasoned about inside Lean, like every other step.)

Three kinds of claim, three grounds

claim earned by refuted by
it has a root one witness, checked (or a proof in a named theory) a proof, in a named theory, that there is none
it has no root with y up to some bound a search to that bound a witness within the bound
it has no root at all a proof, in a named theory one witness

ZTL's judge gives these verdicts (measured, dilemmas/diophantine.py). They show its rules at work on these inputs; they are not evidence that the rules are right:

  • "Pell has a root" is OPEN before the witness and EARNED after it.
  • "Pell has no root", on the search alone, is OPEN; once the witness is in, it is REFUTED. A rule that read the empty search as proof would have given EARNED, and it would have been wrong.
  • "x² = 3y + 2 has no root" is EARNED on the proof and OPEN on a search alone.

A theory's own polynomial

For the polynomial whose rootlessness is ZFC's consistency, the judge's verdict depends on the ground you name. The marks here are cited results, not computations:

  • On the ground ZFC it is OPEN, and on that ground it stays OPEN for good if ZFC is consistent.
  • On the ground "ZFC plus an inaccessible cardinal" it is EARNED relative to that ground, since that stronger theory proves ZFC consistent. The stronger theory's own consistency is in turn not proved by it.
  • If a root were ever found, it would be REFUTED, and ZFC would be inconsistent.

So the asymmetry is sharp: one finite witness could refute the claim, while a search can only ever earn a bounded version of it; the unbounded claim needs a proof, and on the ground ZFC there is none.

What "no axioms" does and does not buy

ZTL's Lean proofs use none of Lean's three standard axioms (see Skipping a check). That is not freedom from incompleteness: Lean's type theory is itself a theory.

Cited. Mario Carneiro (The Type Theory of Lean, 2019) showed that Lean with its axioms is equiconsistent with ZFC plus n inaccessible cardinals, for every n. He has said on the Lean community forum (2022) that he expects the axiom-free fragment to be about as strong, though that is less studied.

My reading. If so, Lean could in principle prove that ZFC's polynomial has no root. If the axiom-free fragment is weaker, it may not. Either way, Lean's own theory has its own such polynomial, which it cannot settle. Independence is relative to a theory, and every consistent theory of this kind (listable, with enough arithmetic) has it. What ZTL adds is not an escape. It names the ground of every "no": a witness against it, a bounded search, a proof in a named theory, or nothing yet.

In the studio

A search that found nothing now has its own kind of ground in ZFL, the table language in which claims reach the judge: search. A row whose status says "verified" but whose ground is such a search is read as not checked. The judge says so and names the cure: prove it, or state the bound the search covered and rest the row on that. You can try it in the studio.

Open

  • No explicit consistency polynomial is computed here; its verdicts rest on cited theorems.
  • How strong axiom-free Lean is, exactly, is not settled.

The code

In the public ZTL repository, github.com/inventor1975/ZTL:

  • lean/ZDiophantine.lean: the Pell witness and the proof for x² = 3y + 2, no axioms. Lean's own lemmas about remainders use an axiom, so the remainders are computed by a function written for the purpose.
  • dilemmas/diophantine.py: the search, the continued fraction and the judge's verdicts, each asserted.
  • In ZFL, the ground kind search and the warning W_SEARCH_NOT_PROOF.

Written with AI assistance (Claude Opus 5.5, Anthropic): the theorems, programs and this text. Idea, direction, editing and responsibility: Vitaly Reznik.