Single-fold Diophantine representations
From OpenAI Aftermath
A single-fold Diophantine representation of a set S of tuples of natural numbers is a polynomial P(a, w) with integer coefficients such that a lies in S exactly when P(a, w) = 0 for some tuple w of natural numbers, and that tuple is then unique. The single-fold conjecture of Davis, Matiyasevich and Robinson asserts that every recursively enumerable set has such a representation; allowing finitely many witnesses gives the finite-fold conjecture. A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a proof of the single-fold conjecture, with a Lean formalization of the main theorem. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- Davis, Putnam and Robinson established exponential Diophantine representations of recursively enumerable relations, Robinson showed how suitable growth conditions yield an existential definition of exponentiation, and Matiyasevich's 1970 construction of an exponentially growing Diophantine relation completed the polynomial representation theorem, which gives the negative solution of Hilbert's tenth problem but does not bound the number of witnesses.
- Matiyasevich proved in 1974 that every recursively enumerable relation has a single-fold exponential representation and reduced the polynomial question to single-fold binary exponentiation. Miller and Shlapentokh obtained single-fold definitions of computably enumerable sets of integers with witnesses in polynomial rings of characteristic zero.
- Cantone, Cuzziol and Omodeo gave a recent account of paired Pell representations and the problem of replacing their exponential cutoff. Poonen used rank-one elliptic curves and denominator growth for Diophantine definitions between rings of integers, and Jones and Matiyasevich developed the bit-masking method for encoding computations.
The original result
- Claim. Theorem 1.1 of Single-fold Diophantine representations states that for every n ≥ 1 and every recursively enumerable set S of n-tuples of natural numbers there is a polynomial P with integer coefficients, in the n parameters and some number m ≥ 1 of unknowns, such that the number of natural-number solutions w of P(a, w) = 0 is 1 when a lies in S and 0 otherwise. Corollary 1.2 states that for some fixed number of unknowns and degree, no algorithm decides solvability in natural numbers of polynomial equations promised to have at most one solution. The manuscript notes that its constants are shown to exist but are not given numerically, and that it makes no claim for the analogous promises over the integers or the rationals.
- Method, as described: the rational points of the rank-one elliptic curve y2 = x3 − 25x give single-fold codes of points whose heights grow quadratically in the index, and a height window selects the index k2 exactly; the resulting growth function cuts off the indices of paired Pell solutions, which yields single-fold exponentiation, and bit-masking with a clock encodes an accepting register-machine run with a unique complete witness.
- Sources. The manuscript Single-fold Diophantine representations at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization establishes the single-fold representation for every recursively enumerable subset of the n-tuples of natural numbers, with exactly one complete witness tuple for members and none for nonmembers, and that the undecidability consequence is not separately formalized. The Comparator statement is
SingleFold.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 21 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statement) | Rates the family "full": the Lean statement is exactly the single-fold representation of every recursively enumerable set, with witnesses in the natural numbers; the undecidability corollary is not separately stated, as the scope note says. Records a sandboxed Comparator pass for SingleFold. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-08 | atimics/math2, Cross-family corollaries of openai/math, entry CL-4 (GitHub, commit 2c0f005) |
Use (written derivation) | Replacing each witness by a sum of four squares, derives that for fixed numbers of unknowns and degree no algorithm decides integer solvability of polynomials promised to have finitely many integer zeros; notes that the number of zeros is not uniformly bounded, so this says nothing about a promise of at most one integer zero. | The catalogue labels each entry by its form of support and states that the entries are conditional on OpenAI's claims. |
| 2026-10-10 | cert-machine, openai/math lane K: run 38019899278 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the SingleFold solution, in 304 s. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list SingleFold, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
