Emre Can Sertöz, Joël Ouaknine, James Worrell
Consortium for Reliability and Reproducibility
A 1-period is a complex number given by the integral of an algebraic function over an algebraic domain, both defined over the algebraic numbers. A famous conjecture of Kontsevich and Zagier states the equality of 1-periods is algorithmically decidable. We prove this conjecture using algorithms that compute a basis for the vector space of 1-periods and their generalized counterparts. We also apply these techniques to effective Lindemann–Weierstrass, to detecting functional dependence of solutions of autonomous first-order (non-linear) differential equations.
Florian Luca, Joël Ouaknine, James Worrell
Mathematical Foundations of Computer Science
The Skolem Problem asks to determine whether a given integer linear recurrence sequence (LRS) has a zero term. This problem whose decidability has been open for many decades, arises across a wide range of topics in computer science, including loop ermination, formal languages, automata theory, and probailistic model checking, amongst many others. In the present paper, we introduce a notion of 'large' zeros of (non-degenerate) linear recurrence sequences, i.e., zeros occurring at an index larger than a sixth-fold exponential of the size of the data defining the given LRS . We establish two main results. First, we show that large zeros are very sparse: the set of positive integers that can possibly arise as large zeros of some LRS has null density. This in turn immediately yields a Universal Skolem Set of density one, answering a question left open in the literature. Second, we define an infinite set of prime numbers, termed 'good', having density one amongst all prime numbers, with the following property: for any large zero of a given LRS, there is an interval around the large zero together with an upper bound on the number of good primes possibly present in that interval. The bound in question is much lower than one would expect if good primes were distributed similarly as ordinary prime numbers, as per the Cramér model in number theory. We therefore conjecture that large zeros do not exist, which would entail decidability of the Skolem Problem.
Joris Nieuwveld, Joël Ouaknine, James Worrell
Mathematical Foundations of Computer Science
Expansions of the monadic second-order (MSO) theory of the structure ⟨N; <⟩have been a fertile and active area of research ever since the publication of the seminal papers of Büchi and Elgot & Rabin on the subject in the 1960s. In the present paper, we establish decidability of the MSO theory of ⟨N; <,P⟩, where P ranges over a large class of unary “dynamical” predicates, i.e., sets of non-negative values assumed by certain integer linear recurrence sequences. One of our key technical tools is the novel concept of (effective) prodisjunctivity, which we expect may also find independent applications further afield.
Piotr Bacik, Joël Ouaknine, David Purser, James Worrell
Consortium for Reliability and Reproducibility
The Skolem Problem asks to determine whether a given linear recurrence sequence (LRS) has a zero term. Showing decidability of this problem is equivalent to giving an effective proof of the Skolem-Mahler-Lech Theorem, which asserts that a non-degenerate LRS has finitely many zeros. The latter result was proven over 90 years ago via an ineffective method showing that such an LRS has only finitely many p-adic zeros. In this paper we consider the problem of determining whether a given LRS has a p-adic zero, as well as the corresponding function problem of computing exact representations of all p-adic zeros. We present algorithms for both problems and report on their implementation. The output of the algorithms is unconditionally correct, and termination is guaranteed subject to the p-adic Schanuel Conjecture (a standard number-theoretic hypothesis concerning the p-adic exponential function). While these algorithms do not solve the Skolem Problem, they can be exploited to find natural-number and rational zeros under additional hypotheses. To illustrate this, we apply our results to show decidability of the Simultaneous Skolem Problem (determine whether two coprime linear recurrences have a common natural-number zero), again subject to the p-adic Schanuel Conjecture.
Toghrul Karimov, Florian Luca, Joris Nieuwveld, Joël Ouaknine, James Worrell
Proceedings of the 2025 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA)
We prove that for any integers α,β>1, the existential fragment of the first-order theory of the structure ⟨ℤ;0,1,<,+,αℕ,βℕ⟩ is decidable (where αℕ is the set of positive integer powers of α, and likewise for βℕ). On the other hand, we show by way of hardness that decidability of the existential fragment of the theory of ⟨ℕ;0,1,<,+,x↦αx,x↦βx⟩ for any multiplicatively independent α,β>1 would lead to mathematical breakthroughs regarding base-α and base-β expansions of certain transcendental numbers.
Transcendence of Hecke-Mahler Series
Florian Luca, Joël Ouaknine, James Worrell
Consortium for Reliability and Reproducibility
We prove transcendence of the Hecke-Mahler series ∑∞n=0f(⌊nθ+α⌋)β−n, where f(x)∈ℤ[x] is a non-constant polynomial α is a real number, θ is an irrational real number, and β is an algebraic number such that |β|>1.
On the Complexity of the Skolem Problem at Low Orders
Piotr Bacik, Joël Ouaknine, James Worrell
Consortium for Reliability and Reproducibility
The Skolem Problem asks to determine whether a given linear recurrence sequence (LRS) ⟨un⟩∞n=0 over the integers has a zero term, that is, whether there exists n such that un=0. Decidability of the problem is open in general, with the most notable positive result being a decision procedure for LRS of order at most 4. In this paper we consider a bounded version of the Skolem Problem, in which the input consists of an LRS ⟨un⟩∞n=0 and a bound N∈ℕ (with all integers written in binary), and the task is to determine whether there exists n∈{0,…,N} such that un=0. We give a randomised algorithm for this problem that, for all d∈ℕ, runs in polynomial time on the class of LRS of order at most d. As a corollary we show that the (unrestricted) Skolem Problem for LRS of order at most 4 lies in 𝖼𝗈𝖱𝖯, improving the best previous upper bound of 𝖭𝖯𝖱𝖯. The running time of our algorithm is exponential in the order of the LRS -- a dependence that appears necessary in view of the 𝖭𝖯-hardness of the Bounded Skolem Problem. However, even for LRS of a fixed order, the problem involves detecting zeros within an exponentially large range. For this, our algorithm relies on results from p-adic analysis to isolate polynomially many candidate zeros and then test in randomised polynomial time whether each candidate is an actual zero by reduction to arithmetic-circuit identity testing.
On the Decidability of Monadic Second-Order Logic with Arithmetic Predicates
Valérie Berthé, Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine, Mihir Vahanwala, James Worrell
ACM/IEEE Symposium on Logic in Computer Science (LICS)
We investigate the decidability of the monadic second-order (MSO) theory of the structure ⟨ℕ;<,P1,…,Pk⟩, for various unary predicates P1,…,Pk⊆ℕ. We focus in particular on "arithmetic" predicates arising in the study of linear recurrence sequences, such as fixed-base powers 𝖯𝗈𝗐k={kn:n∈ℕ}, k-th powers 𝖭k={nk:n∈ℕ}, and the set of terms of the Fibonacci sequence 𝖥𝗂𝖻={0,1,2,3,5,8,13,…} (and similarly for other linear recurrence sequences having a single, non-repeated, dominant characteristic root). We obtain several new unconditional and conditional decidability results, a select sample of which are the following:
∙ The MSO theory of ⟨ℕ;<,𝖯𝗈𝗐2,𝖥𝗂𝖻⟩ is decidable;
∙ The MSO theory of ⟨ℕ;<,𝖯𝗈𝗐2,𝖯𝗈𝗐3,𝖯𝗈𝗐6⟩ is decidable;
∙ The MSO theory of ⟨ℕ;<,𝖯𝗈𝗐2,𝖯𝗈𝗐3,𝖯𝗈𝗐5⟩ is decidable assuming Schanuel's conjecture;
∙ The MSO theory of ⟨ℕ;<,𝖯𝗈𝗐4,𝖭2⟩ is decidable;
∙ The MSO theory of ⟨ℕ;<,𝖯𝗈𝗐2,𝖭2⟩ is Turing-equivalent to the MSO theory of ⟨ℕ;<,S⟩, where S is the predicate corresponding to the binary expansion of 2‾√. (As the binary expansion of 2‾√ is widely believed to be normal, the corresponding MSO theory is in turn expected to be decidable.)
These results are obtained by exploiting and combining techniques from dynamical systems, number theory, and automata theory.
Universal Skolem Sets
Florian Luca, Joël Ouaknine, James Worrell
36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
It is a longstanding open problem whether there is an algorithm to decide the Skolem Problem for linear recurrence sequences, namely whether a given such sequence has a zero term. In this paper we introduce the notion of a Universal Skolem Set: an infinite subset S of the positive integers such that there is an effective procedure that inputs a linear recurrence sequence u = (u(n))n ≥ 0and decides whether u(n) = 0 for some n ∈ S. The main technical contribution of the paper is to exhibit such a set.
Emre Can Sertöz, Joël Ouaknine, James Worrell
Consortium for Reliability and Reproducibility
A 1-period is a complex number given by the integral of an algebraic function over an algebraic domain, both defined over the algebraic numbers. A famous conjecture of Kontsevich and Zagier states the equality of 1-periods is algorithmically decidable. We prove this conjecture using algorithms that compute a basis for the vector space of 1-periods and their generalized counterparts. We also apply these techniques to effective Lindemann–Weierstrass, to detecting functional dependence of solutions of autonomous first-order (non-linear) differential equations.
Florian Luca, Joël Ouaknine, James Worrell
Mathematical Foundations of Computer Science
The Skolem Problem asks to determine whether a given integer linear recurrence sequence (LRS) has a zero term. This problem whose decidability has been open for many decades, arises across a wide range of topics in computer science, including loop ermination, formal languages, automata theory, and probailistic model checking, amongst many others. In the present paper, we introduce a notion of 'large' zeros of (non-degenerate) linear recurrence sequences, i.e., zeros occurring at an index larger than a sixth-fold exponential of the size of the data defining the given LRS . We establish two main results. First, we show that large zeros are very sparse: the set of positive integers that can possibly arise as large zeros of some LRS has null density. This in turn immediately yields a Universal Skolem Set of density one, answering a question left open in the literature. Second, we define an infinite set of prime numbers, termed 'good', having density one amongst all prime numbers, with the following property: for any large zero of a given LRS, there is an interval around the large zero together with an upper bound on the number of good primes possibly present in that interval. The bound in question is much lower than one would expect if good primes were distributed similarly as ordinary prime numbers, as per the Cramér model in number theory. We therefore conjecture that large zeros do not exist, which would entail decidability of the Skolem Problem.
Joris Nieuwveld, Joël Ouaknine, James Worrell
Mathematical Foundations of Computer Science
Expansions of the monadic second-order (MSO) theory of the structure ⟨N; <⟩have been a fertile and active area of research ever since the publication of the seminal papers of Büchi and Elgot & Rabin on the subject in the 1960s. In the present paper, we establish decidability of the MSO theory of ⟨N; <,P⟩, where P ranges over a large class of unary “dynamical” predicates, i.e., sets of non-negative values assumed by certain integer linear recurrence sequences. One of our key technical tools is the novel concept of (effective) prodisjunctivity, which we expect may also find independent applications further afield.
Piotr Bacik, Joël Ouaknine, David Purser, James Worrell
Consortium for Reliability and Reproducibility
The Skolem Problem asks to determine whether a given linear recurrence sequence (LRS) has a zero term. Showing decidability of this problem is equivalent to giving an effective proof of the Skolem-Mahler-Lech Theorem, which asserts that a non-degenerate LRS has finitely many zeros. The latter result was proven over 90 years ago via an ineffective method showing that such an LRS has only finitely many p-adic zeros. In this paper we consider the problem of determining whether a given LRS has a p-adic zero, as well as the corresponding function problem of computing exact representations of all p-adic zeros. We present algorithms for both problems and report on their implementation. The output of the algorithms is unconditionally correct, and termination is guaranteed subject to the p-adic Schanuel Conjecture (a standard number-theoretic hypothesis concerning the p-adic exponential function). While these algorithms do not solve the Skolem Problem, they can be exploited to find natural-number and rational zeros under additional hypotheses. To illustrate this, we apply our results to show decidability of the Simultaneous Skolem Problem (determine whether two coprime linear recurrences have a common natural-number zero), again subject to the p-adic Schanuel Conjecture.
Toghrul Karimov, Florian Luca, Joris Nieuwveld, Joël Ouaknine, James Worrell
Proceedings of the 2025 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA)
We prove that for any integers α,β>1, the existential fragment of the first-order theory of the structure ⟨ℤ;0,1,<,+,αℕ,βℕ⟩ is decidable (where αℕ is the set of positive integer powers of α, and likewise for βℕ). On the other hand, we show by way of hardness that decidability of the existential fragment of the theory of ⟨ℕ;0,1,<,+,x↦αx,x↦βx⟩ for any multiplicatively independent α,β>1 would lead to mathematical breakthroughs regarding base-α and base-β expansions of certain transcendental numbers.
Transcendence of Hecke-Mahler Series
Florian Luca, Joël Ouaknine, James Worrell
Consortium for Reliability and Reproducibility
We prove transcendence of the Hecke-Mahler series ∑∞n=0f(⌊nθ+α⌋)β−n, where f(x)∈ℤ[x] is a non-constant polynomial α is a real number, θ is an irrational real number, and β is an algebraic number such that |β|>1.
On the Complexity of the Skolem Problem at Low Orders
Piotr Bacik, Joël Ouaknine, James Worrell
Consortium for Reliability and Reproducibility
The Skolem Problem asks to determine whether a given linear recurrence sequence (LRS) ⟨un⟩∞n=0 over the integers has a zero term, that is, whether there exists n such that un=0. Decidability of the problem is open in general, with the most notable positive result being a decision procedure for LRS of order at most 4. In this paper we consider a bounded version of the Skolem Problem, in which the input consists of an LRS ⟨un⟩∞n=0 and a bound N∈ℕ (with all integers written in binary), and the task is to determine whether there exists n∈{0,…,N} such that un=0. We give a randomised algorithm for this problem that, for all d∈ℕ, runs in polynomial time on the class of LRS of order at most d. As a corollary we show that the (unrestricted) Skolem Problem for LRS of order at most 4 lies in 𝖼𝗈𝖱𝖯, improving the best previous upper bound of 𝖭𝖯𝖱𝖯. The running time of our algorithm is exponential in the order of the LRS -- a dependence that appears necessary in view of the 𝖭𝖯-hardness of the Bounded Skolem Problem. However, even for LRS of a fixed order, the problem involves detecting zeros within an exponentially large range. For this, our algorithm relies on results from p-adic analysis to isolate polynomially many candidate zeros and then test in randomised polynomial time whether each candidate is an actual zero by reduction to arithmetic-circuit identity testing.
On the Decidability of Monadic Second-Order Logic with Arithmetic Predicates
Valérie Berthé, Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine, Mihir Vahanwala, James Worrell
ACM/IEEE Symposium on Logic in Computer Science (LICS)
We investigate the decidability of the monadic second-order (MSO) theory of the structure ⟨ℕ;<,P1,…,Pk⟩, for various unary predicates P1,…,Pk⊆ℕ. We focus in particular on \"arithmetic\" predicates arising in the study of linear recurrence sequences, such as fixed-base powers \U0001D5AF\U0001D5C8\U0001D5D0k={kn:n∈ℕ}, k-th powers \U0001D5ADk={nk:n∈ℕ}, and the set of terms of the Fibonacci sequence \U0001D5A5\U0001D5C2\U0001D5BB={0,1,2,3,5,8,13,…} (and similarly for other linear recurrence sequences having a single, non-repeated, dominant characteristic root). We obtain several new unconditional and conditional decidability results, a select sample of which are the following:\n ∙ The MSO theory of ⟨ℕ;<,\U0001D5AF\U0001D5C8\U0001D5D02,\U0001D5A5\U0001D5C2\U0001D5BB⟩ is decidable;\n ∙ The MSO theory of ⟨ℕ;<,\U0001D5AF\U0001D5C8\U0001D5D02,\U0001D5AF\U0001D5C8\U0001D5D03,\U0001D5AF\U0001D5C8\U0001D5D06⟩ is decidable;\n ∙ The MSO theory of ⟨ℕ;<,\U0001D5AF\U0001D5C8\U0001D5D0\ 2,\U0001D5AF\U0001D5C8\U0001D5D03,\U0001D5AF\U0001D5C8\U0001D5D05⟩ is decidable assuming Schanuel's conjecture;\n ∙ The MSO theory of ⟨ℕ;<,\U0001D5AF\U0001D5C8\U0001D5D04,\U0001D5AD2⟩ is decidable;\n ∙ The MSO theory of ⟨ℕ;<,\U0001D5AF\U0001D5C8\U0001D5D02,\U0001D5AD2⟩ is Turing-equivalent to the MSO theory of ⟨ℕ;<,S⟩, where S is the predicate corresponding to the binary expansion of 2‾√. (As the binary expansion of 2‾√ is widely believed to be normal, the corresponding MSO theory is in turn expected to be decidable.)\n These results are obtained by exploiting and combining techniques from dynamical systems, number theory, and automata theory.
Universal Skolem Sets
Florian Luca, Joël Ouaknine, James Worrell
36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
It is a longstanding open problem whether there is an algorithm to decide the Skolem Problem for linear recurrence sequences, namely whether a given such sequence has a zero term. In this paper we introduce the notion of a Universal Skolem Set: an infinite subset S of the positive integers such that there is an effective procedure that inputs a linear recurrence sequence u = (u(n))n ≥ 0and decides whether u(n) = 0 for some n ∈ S. The main technical contribution of the paper is to exhibit such a set.
Rich Sequences and Decidability of Logical Theories
Toghrul Karimov, Joris Nieuwveld, Joël Ouaknine
Symposium on Logic in Computer Science (LICS)
We show that for a large class of integer linear recurrence sequences (un)n∈N, the first-order theories of
〈N; <, n ↦ max{0, un}〉 and 〈N; +, {un : n ∈N} ∩ N〉 are undecidable. Our approach is to show that (un)n∈N contains,
in a specific sense, all finite sequences over N, an idea that we borrow from the proof of Hieronymi and Schulz that
the first-order theory of 〈N; +, {2n : n ∈N}, {3n : n ∈N}〉 is undecidable. In a similar way, we harness a contemporary
result about quasi-randomness in the values of the Ramanujan tau function to show that the first-order theory of
〈N; <, n ↦ |τ(n)|〉 is undecidable.
On variable-bounded non-linear Expansions of Presburger arithmetic
Piotr Bacik, Joris Nieuwveld, Joël Ouaknine, Mihir Vahanwala, Madhavan Venkatesh
Symposium on Logic in Computer Science (LICS)
We consider expansions of Presburger arithmetic with families of monadic polynomial predicates. (Examples of such predicates are the set of perfect squares, or the set of integers of the form 2n3-5n+3, etc.)
Although the full attendant first-order theories are well known to be undecidable, very little is known when one restricts the number of variables.
For single-variable theories, we obtain positive results for the following two families of predicates:
(i) for perfect fixed powers, decidability of the corresponding theory follows from the solvability of hyperelliptic Diophantine equations;
and (ii) for polynomials of degree at most three, we establish decidability by relying on the low genus of the resulting algebraic curves.
Finally, we discuss limitations and hardness results (via encodings of longstanding open Diophantine problems) as soon as any of the above restrictions are lifted.
