One solution per member, exactly?
A preprint claims single-fold Diophantine representations for every listable set
Covers result 242 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
4:12. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
A Diophantine equation is a polynomial equation solved in whole numbers. Many sets can be described this way: a is composite exactly when a = (x + 2)(y + 2) for some natural numbers x, y. But such descriptions usually have many witnesses: 12 has four, 24 has six. In 1970, completing work of Davis, Putnam and Robinson, Matiyasevich proved that every set a computer can list has such a description, so Hilbert’s tenth problem is unsolvable. In 1974 he went further for equations that may use exponentiation, giving every listable set a description with exactly one witness, and asked whether plain polynomials can do the same: the single-fold question.
Result 242 is one OpenAI preprint, 27 pages, dated September 24, 2026. It claims that every listable set of tuples of natural numbers has a polynomial description with exactly one tuple of natural-number witnesses for each member, counting every auxiliary variable, and none for nonmembers. If correct, that answers the single-fold question, and with it the finite-fold one. A corollary: deciding solvability stays impossible even when each equation is promised to have at most one solution in natural numbers, with the number of unknowns and the degree fixed.
What it doesn’t claim
An explicit polynomial, its degree or its number of variables; anything over the integers or the rationals. The promise is at most one solution, not exactly one.
Where it stands
- Posted as a preprint
- OpenAI, 27 pages, dated September 24, 2026
- Peer reviewed
- Not yet
- Checked in Lean
- Yes, the main theorem (docs)
Last checked October 19, 2026. The preprint has not been revised since release. In Lean, the main theorem is formalized, about 7,600 lines with no unproved steps, including the elliptic-curve facts the paper takes from textbooks (we did not build it); the promise corollary is not separately formalized. OSVerify has not reviewed it, and we found no expert reaction specific to this result.
How the proof goes
- The cutoff. The classical route needs exponentiation with a unique witness. Matiyasevich’s paired Pell equations nearly give it, but extra solutions creep in unless the witnesses are held below a cutoff that is itself single-fold. The new idea is to use an elliptic curve as the cutoff, building on Poonen’s use of such curves: on y² = x³ − 25x the rational points are nP + t with four choices of t, and the digits of nP grow like n², while Pell solutions grow linearly in digits.
- Squaring an index. A fixed product of heights picks out the point whose index is the square of another’s, with exactly one choice. That gives a single-fold function growing a bit faster than any polynomial but far slower than exponentials, which is enough as the cutoff.
- The classical machinery. Following Jones and Matiyasevich, a program becomes a counter machine whose whole run is packed into the digits of a few huge numbers, checked bit by bit with binomial coefficients, with every helper made unique.
The numbers in the video
- Ours: witness counts for (x + 2)(y + 2) (12 has 4, 24 has 6); a small system for max(a, b) has exactly one solution, but infinitely many without the rule that zeroes the unused case.
- Ours: digits of x(nP) on y² = x³ − 25x, P = (−4, 6), for n = 1 to 12: 1, 4, 7, 14, 20, 30, 41, 53, 67, 83, 100, 119. In a small paired-Pell test (b = 2, n = 3), 6 index pairs pass within our search range without a cutoff (infinitely many in all); with a stand-in cutoff, one survives, giving c = 2³ = 8.
- Ours: a small counter machine’s runs satisfy every equation of the run encoding, and nearby wrong choices fail.
Read the source
- Single-fold Diophantine representations (PDF), 27 pages.
- The Lean formalization notes.
- The collection’s catalog, where this is result 242.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
A Diophantine equation is a polynomial equation where we look for whole-number solutions. Many sets can be described this way: a number a is composite exactly when a equals (x + 2)(y + 2), for some natural numbers x and y. But that description has many witnesses: 12 has four, and 24 has six. In 1970, completing work of Davis, Putnam and Robinson, Matiyasevich proved that every set a computer can list has such a description. So Hilbert’s tenth problem, deciding whether an equation has a solution, is unsolvable. In 1974 Matiyasevich went further for equations that may use exponentiation, giving every listable set such a description with exactly one witness, and asked whether plain polynomials can do the same: the single-fold question. Uniqueness is fragile. Every helper variable counts: a slack for an inequality, a case that is not used, a remainder. Our toy check: a small system for the maximum of two numbers has exactly one solution, but drop the rule that zeroes the unused case and it has infinitely many.
1:13The claim
Result 242 is one OpenAI preprint, 27 pages, dated September 24, 2026. It claims that every listable set of tuples of natural numbers has a polynomial description with exactly one tuple of natural-number witnesses for each member, counting every auxiliary variable, and none for nonmembers. If correct, that answers the single-fold question, and with it the finite-fold one. A corollary: deciding solvability stays impossible even when each equation is promised to have at most one solution in natural numbers, with the number of unknowns and the degree fixed. Not claimed: an explicit polynomial, its degree, or its number of variables; nothing over the integers or the rationals; and the promise is at most one, not exactly one.
2:03How the proof goes
The classical route needs exponentiation with a unique witness. Matiyasevich’s paired Pell equations nearly give it, but extra solutions creep in unless the witnesses are held below a cutoff, which itself must be described with unique witnesses. The new idea is to use an elliptic curve as the cutoff, building on Poonen’s use of such curves: y² = x³ − 25x. Its rational points are the multiples of one point, each shifted by one of four special points, and the number of digits of the n-th multiple grows like n², while Pell solutions grow only linearly in digits. A fixed product of heights can then pick out the point whose index is the square of another’s, with exactly one choice. That gives a single-fold function that grows a bit faster than any polynomial, but far slower than exponentials, which turns out to be enough as the cutoff. In our small Pell test, 6 index pairs pass within our search range without a cutoff, and infinitely many in all; with a stand-in cutoff, one survives, and the answer is 2³ = 8. The rest is the classical machinery of Jones and Matiyasevich. A computer program becomes a counter machine, and its whole run is packed into the digits of a few huge numbers, checked bit by bit with binomial coefficients. Each step is arranged so that every helper is unique. We checked a small machine’s runs against every equation of the run encoding, and that nearby wrong choices fail.
3:34Where it stands
The preprint is unrefereed and unchanged since release. In Lean, the main theorem is formalized, about 7,600 lines with no unproved steps, including the elliptic-curve facts the paper takes from textbooks; the promise corollary is not separately formalized. We did not build it. OSVerify has not reviewed it, and we found no expert reaction specific to this result. If it holds, every listable set has a polynomial equation with exactly one solution for each member, the strengthening Matiyasevich asked for half a century ago.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.