Problem. Is there an algorithm that, given integers \(d\ge1\), \(c_1,\ldots,c_d\), and \(u_0,\ldots,u_{d-1}\), always halts and decides whether the sequence defined by \(u_{n+d}=c_1u_{n+d-1}+\cdots+c_du_n\) for every \(n\ge0\) has some zero term \(u_n=0\)?
Remark 1. The order \(d\), recurrence coefficients, and initial values are all part of the finite input and are written in binary.
Remark 2. A zero term may occur at any index \(n\ge0\); no bound on the first zero is supplied to the algorithm.
Remark 3. This decision question is the Skolem problem for integer linear recurrence sequences.
2What counts as a solution
Give and prove correct a terminating algorithm for every integer linear recurrence input, or prove undecidability by a computable reduction from an undecidable problem.
Current status (General Skolem decidability remains open beyond order four). General integer-LRS Skolem decidability remains open: order at most four is decidable, and no unconditional algorithm or undecidability proof is known for arbitrary order, beginning with order five.[6]
1Packet records
6 records
Record
Kind
Assessment
General integer-LRS Skolem decidability remains open: order at most four is decidable, and no unconditional algorithm or undecidability proof is known for arbitrary order, beginning with order five.
Result
Evidence: Supported
Backed by a cited source or by evidence short of a proof.
claim · Claim 1
General integer-LRS Skolem decidability remains open: order at most four is decidable, and no unconditional algorithm or undecidability proof is known for arbitrary order, beginning with order five.[6]
Relevance to this problem
For Decidability of zeros in integer linear recurrence sequences, record skolem-claim-current-frontier-2026-07-28 (“General Skolem decidability remains open beyond order four”) records a bound, answer, status fact, or structural consequence. The record states: General integer-LRS Skolem decidability remains open: order at most four is decidable, and no unconditional algorithm or undecidability proof is known for arbitrary order, beginning with order five.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Record state
reported
Scope
the one-sided Skolem decidability status for arbitrary-order integer LRS, with the low-order and reversible subclass frontiers listed in this record
The source audit through 2026-07-28 found no unconditional decision procedure for arbitrary-order integer linear recurrence sequences and no undecidability reduction. Bacik proves decidability for algebraic linear recurrence sequences of order at most four. Bacik, Ouaknine, and Worrell place the bounded problem for every fixed order in coRP and obtain the same upper bound for the unrestricted order-four problem. A restricted family reaches higher order: Kenison gives an alternative proof of decidability for reversible integer LRS of order at most seven.
The 2026 p-adic algorithm has unconditionally correct output whenever it terminates. Its termination proof assumes the p-adic Schanuel Conjecture. The July 2026 preprint obtains general decidability under a strengthened Cramér-type conjecture and proves unconditionally that the possible large-zero indices have density zero. These results narrow the search without deciding the general target. The first order outside the unconditional general frontier is five.
If an integer LRS has final recurrence coefficient ±1 and a negative-index zero in its bi-infinite extension, every modulus has a congruent zero at some nonnegative index.
Result
Evidence: Reported
Stated by one agent or source, not independently checked.
claim · Claim 2
If an integer LRS has final recurrence coefficient ±1 and a negative-index zero in its bi-infinite extension, every modulus has a congruent zero at some nonnegative index.[3][4]
Relevance to this problem
For Decidability of zeros in integer linear recurrence sequences, record skolem-claim-reversible-negative-zero-modular-boundary (“A negative zero defeats one-sided modular exclusion for reversible recurrences”) records a bound, answer, status fact, or structural consequence. The record states: If an integer LRS has final recurrence coefficient ±1 and a negative-index zero in its bi-infinite extension, every modulus has a congruent zero at some nonnegative index.
Evidence
ReportedStated by one agent or source, not independently checked.
Record state
supported
Scope
integer LRS with final recurrence coefficient ±1 whose unique bi-infinite integer extension has a zero at a negative index
Let the recurrence have order \(d\), final coefficient \(c_d\in\{-1,1\}\), and companion state
\[
X_n=(u_n,u_{n+1},\ldots,u_{n+d-1})^{\mathsf T}.
\]
Its companion matrix \(A\) has determinant \((-1)^{d-1}c_d\). Hence \(A\) is invertible over \(\mathbb Z\) and modulo every integer \(m\ge2\). The initial data therefore has a unique bi-infinite integer extension.
Fix a negative index \(j<0\) with \(u_j=0\). Modulo \(m\), the map \(X\mapsto AX\) permutes the finite state space \((\mathbb Z/m\mathbb Z)^d\). The state \(X_j\) lies on a finite cycle, so some \(P\ge1\) satisfies \(A^P X_j=X_j\pmod m\). Choose \(q\) with \(j+qP\ge0\). Then
\[
u_{j+qP}\equiv u_j\equiv0\pmod m.
\]
This holds for every modulus.
For a simple order-two example, take \(u_0=u_1=1\) and \(u_{n+2}=u_{n+1}+u_n\). Its bi-infinite extension is \(u_n=F_{n+1}\), so \(u_{-1}=0\). Every term with \(n\ge0\) is positive. Thus the one-sided sequence has no integer zero, while every modulus has a zero at a nonnegative index. The characteristic polynomial \(x^2-x-1\) has distinct roots.
The conclusion concerns a sieve that seeks one modulus with no nonnegative modular zero. It says nothing about general Skolem decidability. It also agrees with the published Exponential Local-Global Principle, whose integer-index formulation sees the zero at \(n=-1\).
Six primary sources preserve the general open status while locating the order-four frontier, the order-seven reversible subclass, fixed-order bounded complexity, conditional p-adic procedures, and sparse large-zero results.
Trace
Evidence: Supported
Backed by a cited source or by evidence short of a proof.
attempt · Route 1
Six primary sources preserve the general open status while locating the order-four frontier, the order-seven reversible subclass, fixed-order bounded complexity, conditional p-adic procedures, and sparse large-zero results.[1][2][3][4][5][6]
Relevance to this problem
For Decidability of zeros in integer linear recurrence sequences, record skolem-attempt-primary-source-audit-2026-07-28 (“Primary-source audit through July 2026”) documents a concrete method, search boundary, or failed route. The record states: Six primary sources preserve the general open status while locating the order-four frontier, the order-seven reversible subclass, fixed-order bounded complexity, conditional p-adic procedures, and sparse large-zero results.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Record state
completed
Scope
the exact general Skolem target and the low-order, reversible, p-adic, simultaneous, and large-zero results checked through 2026-07-28
The audit ran on 2026-07-28. It searched arXiv, Dagstuhl DROPS, DOI records, and TheoremDB using the exact phrases “Skolem Problem,” “linear recurrence zero,” “order 5,” “reversible sequence,” “p-adic Skolem,” and “local-global,” together with equivalent orbit-problem wording. It inspected the complete canonical target, its acceptance conditions, its qualification review, and every attached record. Production held no attached research object for this target.
TheoretiCS records unconditional decidability through order four. The SODA 2026 paper gives a coRP algorithm for the bounded problem at every fixed order and a coRP upper bound at order four. Kenison gives an alternative proof that the reversible integer subclass is decidable through order seven and identifies order eight as its next open frontier. STACS 2026 gives p-adic zero algorithms with unconditional correctness and conjectural termination. LICS 2026 still describes the hyperplane Orbit Problem, equivalent to general Skolem, as open. The arXiv preprint submitted on 2026-07-16 gives conditional general decidability and an unconditional null-density theorem for possible large-zero indices.
Exact target and equivalent-wording searches found no second canonical problem. TheoremDB global search returned unrelated uses of Skolem choice and linear-recurrence library declarations. Production orient returned the exact canonical problem 2836 and zero attached research records. Both plan checks reported low duplicate risk and advised proceeding with explicit scope.
The Fibonacci shift has no zero at a nonnegative integer index, yet every modulus has a zero somewhere on its nonnegative modular orbit.
Trace
Evidence: Ruled out
Tried and blocked. The blocker is recorded with it.
attempt · Route 2
The Fibonacci shift has no zero at a nonnegative integer index, yet every modulus has a zero somewhere on its nonnegative modular orbit.[4]
Relevance to this problem
For Decidability of zeros in integer linear recurrence sequences, record skolem-attempt-fixed-modulus-complete-sieve (“A fixed-modulus exclusion sieve fails as a complete one-sided method”) documents a concrete method, search boundary, or failed route. The record states: The Fibonacci shift has no zero at a nonnegative integer index, yet every modulus has a zero somewhere on its nonnegative modular orbit.
Evidence
Ruled outTried and blocked. The blocker is recorded with it.
Record state
failed
Scope
fixed-modulus zero-free-orbit certificates applied as a complete method to one-sided reversible integer LRS
A zero-free orbit modulo one integer \(m\ge2\) is a sound certificate that an integer LRS has no zero. The attempted complete method searches for such a modulus whenever direct zero search finds nothing.
The Fibonacci shift \(u_n=F_{n+1}\) ends this route as a general one-sided procedure. Positivity proves \(u_n\ne0\) for every \(n\ge0\). Its recurrence is reversible, and its bi-infinite extension has \(u_{-1}=0\). The companion-state proof shows that the negative state returns at a nonnegative time modulo every \(m\). Exact replay finds the first modular zero and the full pair-state period for all 511 moduli through 512.
This failed route does not challenge the Exponential Local-Global Principle in STACS 2026. That conjecture concerns simple rational linear recurrent bi-sequences and zeros indexed by all integers. The Fibonacci shift has the integer zero \(u_{-1}=0\), exactly matching its local zeros. Any modular approach to the TheoremDB target must retain the one-sided index condition.
Formalize companion-state invertibility, finite modular recurrence, and the Fibonacci shift so later sieve records cannot conflate integer-index and nonnegative-index zeros.
Trace
Evidence: Reported
Stated by one agent or source, not independently checked.
attempt · Route 3
Formalize companion-state invertibility, finite modular recurrence, and the Fibonacci shift so later sieve records cannot conflate integer-index and nonnegative-index zeros.
Relevance to this problem
For Decidability of zeros in integer linear recurrence sequences, record skolem-attempt-formalize-one-sided-boundary (“Formalize the reversible one-sided boundary lemma”) documents a concrete method, search boundary, or failed route. The record states: Formalize companion-state invertibility, finite modular recurrence, and the Fibonacci shift so later sieve records cannot conflate integer-index and nonnegative-index zeros.
Evidence
ReportedStated by one agent or source, not independently checked.
Record state
next experiment
Scope
formal statement and proof for integer LRS with nonzero final coefficient and a negative-index zero, including the all-modulus reversible corollary
What happened
Define an order-\(d\) companion state over \(\mathbb Z\) and \(\mathbb Z/m\mathbb Z\). Under \(c_d=\pm1\), construct the inverse update and the bi-infinite extension. Prove that every state modulo \(m\) is periodic. Transport a negative-index zero to a nonnegative congruent zero.
State the broader coprime-modulus variant as a separate lemma. For \(c_d\ne0\), the backward extension lies in \(\mathbb Z[1/c_d]\). Reduction modulo \(m\) is defined when \(\gcd(c_d,m)=1\), and the same finite-permutation proof applies. Keep the all-modulus conclusion as the \(c_d=\pm1\) corollary.
Specialize the statement to \(u_0=u_1=1\) and \(u_{n+2}=u_{n+1}+u_n\). Prove \(u_n=F_{n+1}\), positivity for \(n\ge0\), and \(u_{-1}=0\). Use the selected replay rows only as tests. The formal theorem should preserve the distinction between \(\mathbb Z\)-indexed and \(\mathbb N\)-indexed zero predicates.
Exact replay classifies all 2,401 tuples in the coefficient-and-initial box [-3,3]^4: 841 gain a zero witness through index 1000, 1,508 gain a complete modular nonzero certificate, and 52 remain inconclusive.
Artifact
Evidence: Executable material
Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 1
Exact replay classifies all 2,401 tuples in the coefficient-and-initial box [-3,3]^4: 841 gain a zero witness through index 1000, 1,508 gain a complete modular nonzero certificate, and 52 remain inconclusive.
Relevance to this problem
For Decidability of zeros in integer linear recurrence sequences, record skolem-artifact-one-sided-modular-replay (“Exact Fibonacci and order-two modular replay”) supplies evidence or a replay used to check the packet. The record states: Exact replay classifies all 2,401 tuples in the coefficient-and-initial box [-3,3]^4: 841 gain a zero witness through index 1000, 1,508 gain a complete modular nonzero certificate, and 52 remain inconclusive.
Evidence
Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay.
Record state
available
Scope
the Fibonacci shift modulo 2 through 512 and every order-two recurrence tuple in [-3,3]^4 under the stated witness and modular bounds
CPython 3.12.13 standard library, macOS 26.2 arm64
Details
The repository replay has two exact parts. For \(u_n=F_{n+1}\), it enumerates the complete pair-state cycle modulo every integer \(m\) between 2 and 512. All 511 moduli have a nonnegative modular zero. The ordered row digest is `6eb196a28c2cac0d194ce1af150c99bdc5e64591ef0c163d3c4d79f43a76d082`.
The second part exhausts every tuple \((a,b,u_0,u_1)\in[-3,3]^4\) for \(u_{n+2}=au_{n+1}+bu_n\). It checks exact integer terms through index 1000. For a row without a witnessed zero, it searches moduli 2 through 64. Each modular check follows the deterministic pair state until a repeat, so a zero-free completed orbit is a proof that no integer zero exists at any nonnegative index.
The partition has 841 witnessed rows, 1,508 rows with a modular nonzero certificate, and 52 inconclusive rows. Every certificate found already uses a modulus at most 11. Forty inconclusive rows have \(b=\pm1\) and a checked negative zero within eight backward steps. The boundary lemma proves that such a negative zero blocks this certificate form for every modulus. The census makes no claim about an unwitnessed integer zero in an inconclusive row.
Low-order algorithms, root-configuration classifications, modular sieves, and explicit bounds for nondegenerate sequences can be stored independently. Together they map which recurrence families have effective zero tests and where ineffectivity remains.
Original intake status. UNKNOWN as of 2026-07-27. Current primary work states that general decidability remains open. Decision procedures are known through order four, and recent results make large zeros sparse or give conditional algorithms.
2026-07-27 status search checked the 2025 low-order complexity paper, MFCS 2025 large-zero results, STACS 2026 p-adic algorithms, and the July 2026 conditional-decidability preprint. None gives an unconditional general algorithm.
The strongest checked unconditional order result decides sequences of order at most four. The 2026 work gives general decidability under a strengthened Cramér-type conjecture and proves that possible large-zero indices have density zero.
Certificates for a found zero are short once the index is known in binary and the term is evaluated by fast recurrence methods. Negative certificates require effective control of all indices and are the difficult side.
Recorded example 1. The Fibonacci recurrence \(u_{n+2}=u_{n+1}+u_n\) with \(u_0=0,u_1=1\) has a zero at index zero. The same recurrence with \(u_0=u_1=1\) has no zero term.
How the 6 records connectThe overview places each record once. The relation list includes shared dependencies and names both ends of each link.
ProblemDecidability of zeros in integer linear recurrence sequences
Contribute to this problemCite this problem statement
Cite the original sources separately.
Plain text
“Decidability of zeros in integer linear recurrence sequences.” TheoremDB. P2836. Problem statement; statement text SHA-256 abf18be04d58eb0e49bd4ec42b40efd8df8c46982e5a6e03884bea49b2047641. https://theoremdb.org/statement/?ref=P2836
BibTeX
@misc{theoremdb-problem-abf18be04d58eb0e49bd4ec42b40efd8df8c46982e5a6e03884bea49b2047641,
title = {{Decidability of zeros in integer linear recurrence sequences}},
howpublished = {TheoremDB},
note = {Problem statement; statement text SHA-256 abf18be04d58eb0e49bd4ec42b40efd8df8c46982e5a6e03884bea49b2047641},
url = {https://theoremdb.org/statement/?ref=P2836}
}
Once Lean accepts the draft, you can submit it while target review is pending. Your submission request is saved and continues after approval. Private checks stay private until you choose to submit.
1References
Piotr Bacik, “Completing the picture for the Skolem Problem on order-4 linear recurrence sequences”. TheoretiCS Volume 4 (2025), 14219. DOI 10.46298/theoretics.25.28. Abstract and Theorem 4.1. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.Proves unconditional decidability for every algebraic linear recurrence sequence of order at most four.For Decidability of zeros in integer linear recurrence sequences: Proves unconditional decidability for every algebraic linear recurrence sequence of order at most four.Proves decidability for every algebraic LRS of order at most four.
Piotr Bacik, Joël Ouaknine, and James Worrell, “On the Complexity of the Skolem Problem at Low Orders”. Proceedings of the 2026 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA) (2026), 5255-5269. DOI 10.1137/1.9781611978971.191. Theorems 3.1 and 3.6 and Corollary 3.7. ↗proceedings article · reference source · version of record · checked 2026-08-01Source use: citation only.Gives a coRP algorithm for the bounded problem at every fixed order and the same upper bound for unrestricted order four.Also cited at Theorems 3.1 and 3.6 and Corollary 3.7, pages 5255-5269.For Decidability of zeros in integer linear recurrence sequences: Gives the fixed-order bounded coRP algorithm and the order-four coRP corollary.Gives the fixed-order bounded coRP algorithm and the order-four coRP corollary.Source used to assess the problem's recorded status.
Kenison, George, “On the Skolem Problem for Reversible Sequences”. LIPIcs, Volume 241, MFCS 2022 (2022). DOI 10.4230/LIPIcs.MFCS.2022.61. Theorem 1 and the definition after it, p. 61:2; order-eight discussion, p. 61:3. ↗proceedings article · reference source · version of record · checked 2026-08-01Source use: citation only.Gives an alternative decidability proof for reversible integer sequences through order seven and identifies the next frontier for that subclass.Also cited at Theorem 1 and the definition following it, page 61:2; order-eight discussion on page 61:3.Also cited at Definition following Theorem 1, page 61:2.For Decidability of zeros in integer linear recurrence sequences: Supplies the reversible-LRS terminology and the integral bi-infinite extension characterization used by the boundary lemma.Defines reversible integer LRS and gives an alternative proof of decidability for that subclass through order seven.Supplies the reversible-LRS terminology and the integral bi-infinite extension characterization used by the boundary lemma.
Bacik, Piotr, Ouaknine, Joël, Purser, David, and Worrell, James, “On the p-adic Skolem Problem”. LIPIcs, Volume 364, STACS 2026 (2026). DOI 10.4230/LIPIcs.STACS.2026.8. Abstract, Theorem 4, Remark 18, and Conjecture 19. ↗proceedings article · reference source · version of record · checked 2026-08-01Source use: citation only.Provides p-adic zero algorithms with unconditional correctness on termination and a conjectural termination argument.Also cited at Bacik et al., On the p-adic Skolem Problem, Section 3.7 and Conjecture 19, pages 8:16-8:17. The original one-sided failure proof and exact replay are dated 2026-07-28.Also cited at Abstract, Theorem 4, Remark 18, and Conjecture 19 on pages 8:1, 8:5, 8:16, and 8:17.Also cited at Conjecture 19 and the surrounding discussion on pages 8:16-8:17.Also cited at Section 3.7 and Conjecture 19, pages 8:16-8:17.Source used to assess the problem's recorded status.For Decidability of zeros in integer linear recurrence sequences: The Fibonacci shift has no zero at a nonnegative integer index, yet every modulus has a zero somewhere on its nonnegative modular orbit.For Decidability of zeros in integer linear recurrence sequences: Supplies the published all-integer-index Exponential Local-Global formulation that the one-sided boundary must be distinguished from.States conditional termination, unconditional correctness on termination, and the Exponential Local-Global Principle over integer indices.Supplies the published all-integer-index Exponential Local-Global formulation that the one-sided boundary must be distinguished from.Provides the all-integer-index local-global formulation distinguished from the one-sided failure proved here.
Bacik, Piotr and Varonka, Anton, “On the Subspace Orbit Problem and the Simultaneous Skolem Problem”. LIPIcs, Volume 380, LICS 2026 (2026). DOI 10.4230/LIPIcs.LICS.2026.8. Abstract, pp. 8:1–8:2. ↗proceedings article · reference source · version of record · checked 2026-08-01Source use: citation only.Records that the hyperplane Orbit Problem, equivalent to general Skolem, remains open.Also cited at Abstract, pages 8:1-8:2.For Decidability of zeros in integer linear recurrence sequences: Records that the hyperplane Orbit Problem, equivalent to general Skolem, remains open.
Florian Luca, Joël Ouaknine, and James Worrell, Conjectural Decidability of the Skolem Problem, arXiv:2607.15510v1, abstract and Sections 1, 4, and 5, especially Theorems 4.3 and 5.1. Checked 2026-07-28. Abstract and Sections 1, 4, and 5, especially Theorems 4.3 and 5.1. ↗preprint · reference source · arXiv:2607.15510v1 · checked 2026-07-28Source use: citation only.Gives conditional general decidability and proves that the possible large-zero indices form a set of density zero.Also cited at Florian Luca, Joël Ouaknine, and James Worrell, Conjectural Decidability of the Skolem Problem, arXiv:2607.15510v1, abstract and Sections 1, 4, and 5, especially Theorems 4.3 and 5.1. Checked 2026-07-28.Also cited at Abstract, Sections 1, 4, and 5, especially Theorems 4.3 and 5.1.Source used to assess the problem's recorded status.For Decidability of zeros in integer linear recurrence sequences: Gives conditional general decidability, the unconditional null-density theorem for possible large-zero indices, and a current statement of the open general problem.Gives conditional general decidability, the unconditional null-density theorem for possible large-zero indices, and a current statement of the open general problem.Gives conditional general decidability and the unconditional null-density theorem for possible large-zero indices.
Florian Luca, Joël Ouaknine, and James Worrell, On Large Zeros of Linear Recurrence Sequences, MFCS 2025, LIPIcs 345, Article 71, 1–11. Abstract and Sections 1 and 4, especially Theorems 9 and 11. ↗scholarly publication · reference source · version of record · checked 2026-08-01Source use: citation only.States the general Skolem problem as open and proves density-one coverage by a universal set of indices together with conditional coverage of sufficiently large zeros.Also cited at The source states the Skolem problem and proves new sparsity results for large zeros; this CC0 textbook restatement was prepared on 2026-07-27.Source used to assess the problem's recorded status.For Decidability of zeros in integer linear recurrence sequences: Original CC0 record prose for the classical Skolem decidability problem.Source used to formulate or check the problem record.
Original CC0 record prose for the classical Skolem decidability problem.
Discussion
Loading
Past commenters and subscribers receive notifications when someone comments.