Single-fold Diophantine representations and undecidability under an at-most-one-solution promise

Every recursively enumerable set of tuples of natural numbers has a Diophantine representation with exactly one auxiliary solution for each member and none for nonmembers. This proves the single-fold conjecture and hence the finite-fold conjecture. Diophantine solvability over the nonnegative integers remains undecidable even with an at-most-one-solution promise. (Lean)

Manuscript

Single-fold Diophantine representations

September 24, 2026 · source · Lean formalization available · cite as \cite{OAI:Single-fold-Diophantine-representations-September-24-2026}

Every recursively enumerable set of natural-number tuples has a polynomial Diophantine representation with exactly one complete auxiliary tuple for each member. This proves the single-fold conjecture and, consequently, the finite-fold conjecture.

Result 242 · Mathematical logic. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.