Books

The 13 problem files in FormalConjectures/Books that state a research or textbook statement, at commit 2055e5ad, one article each.

Their docstrings and Lean statements are quoted from Formal Conjectures (Google DeepMind) at that commit, under its Apache-2.0 license.

TheoremConvergence of the Borwein Series with Sinusoidal Coefficient#

References: - MathWorld, Harmonic Series - Borwein, J.; Bailey, D.; Girgensohn, R. Experimentation in Mathematics: Computational Paths to Discovery, A K Peters, 2004, p. 56.

Quoted from FormalConjectures/Books/BorweinSineSeries.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved.

BorweinSineSeries.borwein_sine_series

Solved: stated here; a Lean proof is at https://github.com/AxiomMath/gdm-formal-conjectures/blob/main/BorweinSineSeries/solution.lean.

Does the series

\[ \sum_{n=1}^{\infty} \frac{\left(\frac{2}{3} + \frac{1}{3}\sin n\right)^n}{n} \]

converge?

After computing approximately \(10^7\) terms, the partial sums approximate \(2.163\).

See https://arxiv.org/abs/2007.11017 for a proof of the convergence, relying on an irrationality measure for pi.

Also see https://github.com/AxiomMath/gdm-formal-conjectures/blob/main/docs/BorweinSineSeries.md for a partial formalization of the conjecture, conditional on such an irrationality measure of pi (cf https://arxiv.org/abs/1912.06345).

theorem borwein_sine_series :
    Summable fun n : ℕ+ ↦ ((2 / 3 + 1 / 3 * Real.sin (n : ℝ)) ^ (n : ℕ)) / (n : ℝ)

Category research solved; AMS 26 Real functions, 40 Sequences, series, summability. Declared in FormalConjectures/Books/BorweinSineSeries.lean, line 52.

Sources

• FormalConjectures/Books/BorweinSineSeries.lean at 2055e5ad
• MathWorld, Harmonic Series

LeanBorweinSineSeries.borwein_sine_series

TheoremBugeaud Collection of Conjectures and Open Questions: Fractional Parts of Powers#

Chapter 10 of the book collects open questions. This file formalizes Problems 10.1, 10.2, 10.3 and the unnumbered conjecture by Waldschmidt.

References: - [Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10. - [Har19] Hardy, Gr H. "A problem of Diophantine approximation." J. Indian Math. Soc 11 (1919): 162-166. - [Kok45] Koksma, J. F. "Sur la théorie métrique des approximations diophantiques." Indag. Math 7 (1945): 54-70. - [Mah53] Mahler, Kurt. "On the approximation of logarithms of algebraic numbers." Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences 245.898 (1953): 371-398. - Wal03 Waldschmidt, Michel. "Linear independence measures for logarithms of algebraic numbers." Diophantine Approximation: Lectures given at the CIME Summer School held in Cetraro, Italy, June 28–July 6, 2000. Berlin, Heidelberg: Springer Berlin Heidelberg, 2003. 249-344.

Quoted from FormalConjectures/Books/BugeaudDistributionModuloOne/IntDistanceDistribution.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 4 research or textbook statements: 4 open. It also has 1 test statement, counted here but not shown.

Bugeaud01.problem_10_1

Open: stated without proof.

Problem 10.1. Are there a transcendental number \(\alpha\) and a positive real number \(\xi\) such that \(\lVert \xi \alpha^n \rVert\) tends to~\(0\) as~\(n\) tends to infinity? [Har19] (Trivial for \(|\alpha| < 1\))

theorem problem_10_1 :
    ∃ (α ξ : ℝ), 1 < |α| ∧ Transcendental ℚ α ∧ 0 < ξ ∧
      Filter.Tendsto (fun n : ℕ ↦ distToNearestInt (ξ * α ^ n)) Filter.atTop (nhds 0)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/IntDistanceDistribution.lean, line 52.

Bugeaud01.problem_10_2

Open: stated without proof.

Problem 10.2. To prove that \(\lVert e^n \rVert\) does not tend to 0 as n tends to infinity.

theorem problem_10_2 :
    ¬ Filter.Tendsto (fun n : ℕ ↦ distToNearestInt (Real.exp n)) Filter.atTop (nhds 0)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/IntDistanceDistribution.lean, line 62.

Bugeaud01.problem_10_3

Open: stated without proof.

Problem 10.3. To prove that there exists a positive real number~\(c\) such that \(\lVert e^n \rVert > e^{−cn}\), for every~\(n \ge 1\). Posed by Mahler [Mah53].

theorem problem_10_3 :
    ∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 1 ≤ n → Real.exp (-c * n) < distToNearestInt (Real.exp n)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/IntDistanceDistribution.lean, line 71.

Bugeaud01.waldschmidt

Open: stated without proof.

Waldschmidt [Wal03] conjectured that a stronger result holds, namely that there exists a positive real number~\(c\) such that \(\lVert e^n \rVert > n^{-c}\) for every~\(n \ge 2\). This is supported by metrical results [Kok45].

Note: the bound \(n^{-c}\) equals \(1\) when \(n = 1\) for all \(c\), while the distance to the nearest integer is always at most \(1/2\), so the conjecture must start at \(n \ge 2\).

theorem waldschmidt :
    ∃ c : ℝ, 0 < c ∧ ∀ n : ℕ, 2 ≤ n → (n : ℝ) ^ (-c) < distToNearestInt (Real.exp n)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/IntDistanceDistribution.lean, line 84.

Sources

• FormalConjectures/Books/BugeaudDistributionModuloOne/IntDistanceDistribution.lean at 2055e5ad
• Wal03

LeanBugeaud01.problem_10_1 · Bugeaud01.problem_10_2 · Bugeaud01.problem_10_3 · Bugeaud01.waldschmidt

TheoremNormal and rich numbers and the sequence \((b^n \xi)\) modulo one#

Let \(b \ge 2\) be an integer. A real number \(\xi\) is normal in base \(b\) if and only if the sequence \((b^n \xi)_{n \ge 0}\) is uniformly distributed modulo one. This was proved by Wall [Wal49]; see also [Bug12, Theorem 4.14] and [EvdPSW03, p. 127].

A real number \(\xi\) is rich (or disjunctive) in base \(b\) if every finite block of digits occurs in its base-\(b\) expansion. By the same argument, \(\xi\) is rich in base \(b\) if and only if the sequence \((b^n \xi)_{n \ge 0}\) is dense modulo one [Bug12, Section 4.4].

The two easy implications, normal implies rich and uniformly distributed implies dense, are NormalNumber.IsNormalInBase.isRichInBase and IsEquidistributedModuloOne.dense_range.

References: - [Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Cambridge Tracts in Mathematics 193. Cambridge University Press, 2012. Chapter 4. - [Wal49] Wall, Donald Dines. "Normal numbers." Ph.D. thesis, University of California, Berkeley, 1949. - [EvdPSW03] Everest, Graham, Alf van der Poorten, Igor Shparlinski, and Thomas Ward. "Recurrence sequences." Mathematical Surveys and Monographs 104. American Mathematical Society, Providence, RI, 2003.

Quoted from FormalConjectures/Books/BugeaudDistributionModuloOne/NormalAndRich.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 2 research or textbook statements: 1 solved and 1 textbook result.

BugeaudNormalAndRich.isNormalInBase_iff_isEquidistributedModuloOne

Solved: stated here; a Lean proof is at https://github.com/rwst/formal-conjectures/blob/a522a5352dd28df0b5ef08c213c368b5f6a5df6e/FormalConjectures/Books/BugeaudDistributionModuloOne/NormalAndRich.lean#L459.

A real number \(\xi\) is normal in base \(b\) if and only if \((b^n \xi)_{n \ge 0}\) is uniformly distributed modulo \(1\) [Wal49], [Bug12, Theorem 4.14].

theorem isNormalInBase_iff_isEquidistributedModuloOne (b : ℕ) (hb : 2 ≤ b) (ξ : ℝ) :
    IsNormalInBase b ξ ↔ IsEquidistributedModuloOne fun n => (b : ℝ) ^ n * ξ

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/NormalAndRich.lean, line 55.

BugeaudNormalAndRich.isRichInBase_iff_dense

Textbook result, stated without proof. A Lean proof is at https://github.com/rwst/formal-conjectures/blob/a522a5352dd28df0b5ef08c213c368b5f6a5df6e/FormalConjectures/Books/BugeaudDistributionModuloOne/NormalAndRich.lean#L466.

A real number \(\xi\) is rich in base \(b\) if and only if \((b^n \xi)_{n \ge 0}\) is dense modulo \(1\) [Bug12, Section 4.4].

theorem isRichInBase_iff_dense (b : ℕ) (hb : 2 ≤ b) (ξ : ℝ) :
    IsRichInBase b ξ ↔ Dense (Set.range fun n => (↑((b : ℝ) ^ n * ξ) : AddCircle (1 : ℝ)))

Category textbook; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/NormalAndRich.lean, line 63.

Sources

• FormalConjectures/Books/BugeaudDistributionModuloOne/NormalAndRich.lean at 2055e5ad

LeanBugeaudNormalAndRich.isNormalInBase_iff_isEquidistributedModuloOne · BugeaudNormalAndRich.isRichInBase_iff_dense

TheoremBugeaud Collection of Conjectures and Open Questions: Spectrum of Sequence#

References: - [Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10. - [Men73] Mendès France, Michel. "Les ensembles de Bésineau." Séminaire Delange-Pisot-Poitou 15.1 (1973): 1-6. - [Özc26] Özcan, Hikmet Burak. "The spectrum of \((\xi\alpha^n)\) can be uncountable." arXiv:2609.07714 (2026).

Counterexample

Problem 10.4 is false. Özcan [Özc26] proves that for every real \(\alpha > 1\) there are \(2^{\aleph_0}\) reals \(\xi > 0\) whose spectrum contains one and the same uncountable set. The counterexample below is an independent, self-contained instance of this for the base \(\alpha = 64\), where the digits of \(\xi\) can be prescribed directly.

For a bit sequence \(u \in \{0, 1\}^{\mathbb{N}}\) put

\[\theta_u = \sum_{i \ge 0} (1 + u_i) \, 8^{-e(i)}, \qquad e(i) = 4^{i+1} + i + 6.\]

The map \(u \mapsto \theta_u\) is injective with values in \((0, 1)\).

Split the indices into the blocks \([5 m_k, 6 m_k)\) with \(m_k = 20 \cdot 8^k\); these are pairwise disjoint. Block number \(k = \langle L, c \rangle\), where \(\langle \cdot, \cdot \rangle\) is the Cantor pairing, is reserved for the bit string \(c\) of length \(L\). On that block the base-\(64\) digits of \(\xi\) are chosen so that \(\{\xi 64^n\}\) shadows \(\{n \theta\}\) for every \(\theta\) whose first \(L\) bits are \(c\). This is possible because one base-\(64\) digit pins down \(\{\xi 64^n\}\) up to \(2/64\), and because \(k \le 4^{L+1}\) forces the block to sit far to the left of the precision \(8^{-e(L)}\) of the truncation of \(\theta\), so that \(n\) times the truncation error stays below \(1/512\) on the block.

Consequently \(\{\xi 64^n - n \theta_u\} < 1/10\) for all \(n\) in the block attached to the first \(L\) bits of \(u\), for every \(L\). That block is the last sixth of \([0, 6 m_k)\), so at the times \(N = 6 m_k - 6\) at most a proportion \(5/6\) of the points \(\{\xi 64^n - n\theta_u\}\) with \(n < N\) lies in \([1/10, 1]\), whereas uniform distribution modulo one would force the proportion \(9/10\). Hence every irrational \(\theta_u\) lies in the spectrum of \((\xi 64^n)\), and since \(\{\theta_u\}\) is uncountable the spectrum cannot be countable.

Quoted from FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_4.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 solved.

Bugeaud04.spectrum_xi_alpha_pow_countable

Solved: stated here; a Lean proof is at https://github.com/mo271/formal-conjectures/blob/8e2413a849b19822431772684d41cdc31637a409/FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_4.lean#L682.

Problem 10.4. Let \(\xi\) be a non-zero real number and \(\alpha > 1\) be a real number. Is the spectrum of the sequence \((\xi \alpha^n)_{n \ge 1}\) at most countable? Posed by Mendès France [Men73].

The answer is no. Özcan [Özc26] disproved this for every \(\alpha > 1\); the counterexample formalised here takes \(\alpha = 64\) and the real number $\xi = $ xiVal, whose spectrum contains the uncountable set of irrational numbers of the form thetaSeq u.

theorem spectrum_xi_alpha_pow_countable :
    ¬ ∀ (ξ : ℝ), ξ ≠ 0 → ∀ (α : ℝ), 1 < α → (Spectrum (fun n => ξ * α ^ n)).Countable

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_4.lean, line 82.

Sources

• FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_4.lean at 2055e5ad
• arXiv:2609.07714

LeanBugeaud04.spectrum_xi_alpha_pow_countable

TheoremBugeaud Collection of Conjectures and Open Questions: Lacunary Sequences in Real Number Fields#

The following problems were proposed and discussed by Dubickas as Conjecture 2 in [Dub09].

References: - [Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10. - [Dub09] Dubickas, Artūras. "An approximation property of lacunary sequences." Israel Journal of Mathematics 170.1 (2009): 95-111.

Quoted from FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_5.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 2 research or textbook statements: 2 solved. It also has 1 test statement, counted here but not shown.

Bugeaud05.problem_10_5

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/bugeaud-10-5-lacunary/blob/fa5533b0229a19f2092c777cadb43ef4b0f2600b/lean/Bugeaud105/Compatibility.lean#L18-L19.

Problem 10.5 (first part). Let \(\mathbb{K}\) be a real number field. Then, for any \(\varepsilon > 0\), there exists a lacunary sequence \((t_n)_{n \ge 1}\) of positive numbers in \(\mathbb{K}\) such that

\[\limsup_{n \to \infty} \{\xi t_n\} \ge 1 - \varepsilon,\]

for any real number \(\xi\) not in \(\mathbb{K}\).

This follows from the stronger problem_10_5_moreover via problem_10_5_of_moreover. A Lean 4 formalization by Kenta Kitamura (KitaKen1 on GitHub) is available at KitaKen1/bugeaud-10-5-lacunary.

theorem problem_10_5 (K : IntermediateField ℚ ℝ) [FiniteDimensional ℚ K]
    {ε : ℝ} (hε : 0 < ε) :
    ∃ t : ℕ → K, (∀ n, 0 < (t n : ℝ)) ∧
      IsLacunaryReal (fun k => (t k : ℝ)) ∧
      ∀ ξ : ℝ, ξ ∉ K →
        (1 - ε) ≤ limsup (fun n => Int.fract (ξ * (t n : ℝ))) atTop

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_5.lean, line 54.

Bugeaud05.problem_10_5_moreover

Solved: stated here; a Lean proof is at https://github.com/KitaKen1/bugeaud-10-5-lacunary/blob/fa5533b0229a19f2092c777cadb43ef4b0f2600b/lean/Bugeaud105/Compatibility.lean#L14-L16.

Problem 10.5 ("moreover" clause). With the same hypotheses as problem_10_5, the sequence \((t_n)\) can be chosen so that, for any real \(\xi\) not in \(\mathbb{K}\), each subinterval of \([0, 1]\) of length \(\varepsilon\) contains a limit point of the sequence \((\{\xi t_n\})_{n \ge 1}\). This is strictly stronger than problem_10_5: the limsup bound is the special case at the subinterval \([1 - \varepsilon, 1]\).

A Lean 4 formalization by Kenta Kitamura (KitaKen1 on GitHub) proves this statement using the explicit positive integer sequence

\[t_{Jk+r} = (J+r)2^k \qquad (k \ge 0,\ 0 \le r < J).\]

Here \(Q\) is a positive integer chosen so that \(Q > 1/\varepsilon\), and \(J = 10Q!\). Since \(\mathbb{K}\) contains \(\mathbb{Q}\), every term belongs to \(\mathbb{K}\). The proof verifies that this sequence is lacunary and has the required cluster-point property simultaneously for every \(\xi \notin \mathbb{K}\). See KitaKen1/bugeaud-10-5-lacunary.

theorem problem_10_5_moreover (K : IntermediateField ℚ ℝ) [FiniteDimensional ℚ K]
    {ε : ℝ} (hε : 0 < ε) :
    ∃ t : ℕ → K, (∀ n, 0 < (t n : ℝ)) ∧
      IsLacunaryReal (fun k => (t k : ℝ)) ∧
      ∀ ξ : ℝ, ξ ∉ K → ∀ a, a ∈ Set.Icc (0 : ℝ) (1 - ε) →
        ∃ y ∈ Set.Icc a (a + ε),
          MapClusterPt y atTop (fun n => Int.fract (ξ * (t n : ℝ)))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_5.lean, line 83.

Sources

• FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_5.lean at 2055e5ad

LeanBugeaud05.problem_10_5 · Bugeaud05.problem_10_5_moreover

TheoremBugeaud Collection of Conjectures and Open Questions: Rapidly Increasing Sequences Dense Modulo One#

Problem 10.6 asks for a "very rapidly increasing" sequence \((m_n)_{n \ge 1}\) of positive integers with \((\{\xi m_n\})_{n \ge 1}\) dense modulo one for every irrational \(\xi\). The informal phrase admits several readings, and they are not equivalent:

• a lower bound on the size of the terms, \(m_n \ge f(n)\);
• an upper bound on the counting function of \(\{m_n\}\);
• a lower bound on the consecutive ratios, \(m_{n+1}/m_n \ge 1 + c/\log n\).

The first two readings are vacuous, and exists_dense_of_growth_and_sparsity below says so: a sequence built from runs of consecutive integers is dense modulo one for every irrational \(\xi\) by an elementary argument, and the runs may be placed so that its terms dominate any prescribed \(f\) while its counting function stays below \((\log\log N)^2\). In the subexponential range the growth half is a special case of [Bos83, Thm. 1.5], which produces such a sequence in any prescribed subexponential corridor and in the stronger uniform-distribution form; the sparsity half sits below the \(\log N\) floor that every sublacunary sequence obeys, and so below the counting function of [Kat16, Cor. 4.10]. Consequently problem_10_6_variant_2, which asks only for intermediate growth, is not open.

The third reading is IsGenuinelySublacunary, and it is the only one with content: it implies the first (hasIntermediateGrowth_of_isGenuinelySublacunary), and it is not answered by runs, since inside a run \(m_{n+1} - m_n = 1\). That reading is problem_10_6_variant_1, which remains open; [Kat16, Cor. 4.9] gives a universally densifying sequence of multiplicative shape \(\{2^n 3^e\}\) whose ratio behaviour reduces the question to a Diophantine statement about \(\log_2 3\).

The three statements that need a long proof carry a formal_proof link to the version of this file that contains it: the construction by runs, its counting function, and the growth estimate behind hasIntermediateGrowth_of_isGenuinelySublacunary.

References: - [Bos83] Boshernitzan, Michael D. "Homogeneously distributed sequences and Poincaré sequences of integers of sublacunary growth." Monatshefte für Mathematik 96.3 (1983): 173-181. - [Bos94] Boshernitzan, Michael D. "Density modulo 1 of dilations of sublacunary sequences." Advances in Mathematics 108.1 (1994): 104-117. - [Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10. - [Fur67] Furstenberg, H. "Disjointness in ergodic theory, minimal sets, and a problem in diophantine approximation". Math. Systems Theory 1, 1–49 (1967). - [Kat16] Katz, Asaf. "Generalizations of Furstenberg's Diophantine result." arXiv:1607.00670 (2016). - [Mat80] de Mathan, Bernard. "Numbers contravening a condition in density modulo 1." Acta Mathematica Hungarica 36.3-4 (1980): 237-241. - [Pol79] Pollington, Andrew Douglas. "On the density of sequence ${n_ {k}\xi} $." Illinois Journal of Mathematics 23.4 (1979): 511-515.

Quoted from FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_6.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 7 research or textbook statements: 1 open and 6 solved. It also has 3 test statements and 2 API statements, counted here but not shown.

Bugeaud06.pollington_de_mathan

Solved: stated here without proof.

The Pollington–de Mathan theorem [Pol79][Mat80]. For every lacunary sequence \((m_n)_{n \ge 1}\) of positive integers, the set of real numbers \(\xi\) for which \((\{\xi m_n\})_{n \ge 1}\) is not dense modulo one has full Hausdorff dimension.

theorem pollington_de_mathan (m : ℕ → ℕ) (hm : ∀ n, 0 < m n) (hlac : IsLacunary m) :
    dimH {ξ : ℝ | ¬ Dense (Set.range fun n => (↑(ξ * m n) : AddCircle (1 : ℝ)))} = 1

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_6.lean, line 81.

Bugeaud06.furstenberg_two_three

Solved: stated here without proof.

Furstenberg's theorem [Fur67] (the \(\times 2, \times 3\) case). For every irrational number \(\xi\), the two-parameter family \((\{\xi \, 2^m 3^n\})_{m, n \ge 1}\) is dense modulo one.

theorem furstenberg_two_three (ξ : ℝ) (hξ : Irrational ξ) :
    Dense {x : AddCircle (1 : ℝ) |
      ∃ m n : ℕ, 0 < m ∧ 0 < n ∧ x = ↑(ξ * (2 ^ m * 3 ^ n : ℕ))}

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_6.lean, line 89.

Bugeaud06.boshernitzan

Solved: stated here without proof.

Boshernitzan's theorem [Bos94]. Given a real sublacunary sequence \(r\), the set of real numbers \(\xi\) for which \((\{\xi r_n\})_{n \ge 1}\) is not dense modulo one has Hausdorff dimension zero.

theorem boshernitzan (r : ℕ → ℝ) (hr : ∀ n, 0 < r n) (hunb : ¬ BddAbove (Set.range r))
    (hsub : Tendsto (fun n => r (n + 1) / r n) atTop (nhds 1)) :
    dimH {ξ : ℝ | ¬ Dense (Set.range fun n => (↑(ξ * r n) : AddCircle (1 : ℝ)))} = 0

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_6.lean, line 98.

Bugeaud06.exists_dense_of_growth

Solved: stated here; a Lean proof is at https://github.com/rwst/formal-conjectures/blob/63c3e7233f1e512ea2474f35f4f2cd70624583f6/FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_6.lean#L398.

A lower bound on the size of the terms cannot make Problem 10.6 nontrivial. For every growth demand f there is a strictly increasing sequence dominating f at every index which is dense modulo one for every irrational \(\xi\).

In the subexponential range this is a special case of [Bos83, Thm. 1.5], which produces such a sequence inside any prescribed corridor \([n_k, m_k)\) with \(m_k - n_k \to \infty\) and \(m_k / n_k \to 1\), and in the stronger form of uniform distribution; the elementary construction of the linked proof is uniform in f and has no growth ceiling.

theorem exists_dense_of_growth (f : ℕ → ℕ) :
    ∃ m : ℕ → ℕ, StrictMono m ∧ (∀ n, f n ≤ m n) ∧
      ∀ ξ : ℝ, Irrational ξ →
        Dense (Set.range fun n => (↑(ξ * m n) : AddCircle (1 : ℝ)))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_6.lean, line 123.

Bugeaud06.exists_dense_of_growth_and_sparsity

Solved: stated here; a Lean proof is at https://github.com/rwst/formal-conjectures/blob/63c3e7233f1e512ea2474f35f4f2cd70624583f6/FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_6.lean#L411.

Neither can an upper bound on the counting function, even together with the growth demand. The same sequence dominates an arbitrary f and has counting function below \((\log\log N)^2\) — an exponential below the \(\log N\) floor that every sublacunary sequence obeys, and so below the counting function of [Kat16, Cor. 4.10]. So a reading of "very rapidly increasing" that constrains only the size of the terms or the sparsity of their range leaves Problem 10.6 with no content.

theorem exists_dense_of_growth_and_sparsity (f : ℕ → ℕ) :
    ∃ m : ℕ → ℕ, StrictMono m ∧ (∀ n, f n ≤ m n) ∧
      (∀ᶠ N : ℕ in atTop, (countingFn m N : ℝ) ≤ (Real.log (Real.log N)) ^ 2) ∧
      ∀ ξ : ℝ, Irrational ξ →
        Dense (Set.range fun n => (↑(ξ * m n) : AddCircle (1 : ℝ)))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_6.lean, line 138.

Bugeaud06.problem_10_6_variant_1

Open: stated without proof.

Problem 10.6. Find a very rapidly increasing sequence \((m_n)_{n \ge 1}\) of positive integers such that \((\{\xi m_n\})_{n \ge 1}\) is dense modulo one for every irrational number \(\xi\). Note: Furstenberg's \(2^m3^n\) is sublacunary but requires two parameters.

This is the reading of "very rapidly increasing" as a lower bound on the consecutive ratios, and it is the one that remains open. It is not answered by runs of consecutive integers, since inside a run \(m_{n+1} - m_n = 1\); and by not_isLacunary_of_dense any answer is pinched between a decaying ratio floor and the failure of lacunarity. [Kat16, Cor. 4.9] gives a universally densifying sequence of the multiplicative shape \(\{2^n 3^e\}\), for which the ratio condition reduces to a Diophantine statement about the differences of the exponents \(e\) times \(\log_2 3\) modulo one.

theorem problem_10_6_variant_1 :
    ∃ m : ℕ → ℕ,
    StrictMono m ∧
    IsGenuinelySublacunary m ∧
    ∀ ξ : ℝ, Irrational ξ →
      Dense (Set.range fun n => (↑(ξ * m n) : AddCircle (1 : ℝ)))

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_6.lean, line 250.

Bugeaud06.problem_10_6_variant_2

Proved here.

Problem 10.6, intermediate-growth variant. This asks only for a lower bound on the size of the terms, and under that reading the problem is not open: runs of consecutive integers answer it, by exists_dense_of_growth applied to \(f(n) = \lceil e^n \rceil\). The witness below is exhibited at \(\alpha = 1/2\); the same sequence works for every \(\alpha < 1\), since \(\exp(n^\alpha) \le \exp(n) \le f(n)\) there.

The result is not new: [Bos83, Thm. 1.5] gives a sequence of any prescribed subexponential growth that is uniformly distributed — not merely dense — modulo one for every irrational dilate.

theorem problem_10_6_variant_2 :
    ∃ m : ℕ → ℕ,
    StrictMono m ∧
    (∃ α : ℝ, 0 < α ∧ α < 1 ∧ HasIntermediateGrowth α m) ∧
    ∀ ξ : ℝ, Irrational ξ →
      Dense (Set.range fun n => (↑(ξ * m n) : AddCircle (1 : ℝ)))

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_6.lean, line 268.

Sources

• FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_6.lean at 2055e5ad

LeanBugeaud06.pollington_de_mathan · Bugeaud06.furstenberg_two_three · Bugeaud06.boshernitzan · Bugeaud06.exists_dense_of_growth · Bugeaud06.exists_dense_of_growth_and_sparsity · Bugeaud06.problem_10_6_variant_1 · Bugeaud06.problem_10_6_variant_2

TheoremBugeaud Collection of Conjectures and Open Questions: Confined Powers of Non-Pisot Numbers#

References: - [Bug12a] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10. - [Bug12b] Bugeaud, Yann, and Nikolay Moshchevitin. "On fractional parts of powers of real numbers close to 1." Mathematische Zeitschrift 271.3 (2012): 627-637.

Quoted from FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_7.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 1 research or textbook statement: 1 open.

Bugeaud07.problem_10_7

Open: stated without proof.

Problem 10.7. Let \(\varepsilon\) be a positive real number. Are there arbitrarily large real numbers \(\alpha\) such that \(\alpha\) is not a Pisot number and all the fractional parts \(\{\alpha^n\}\), \(n \ge 1\), are lying in an interval of length \(\varepsilon / \alpha\)? [Bug12b]

theorem problem_10_7 :
    ∀ ε : ℝ, 0 < ε → ∀ M : ℝ, ∃ α : ℝ, M < α ∧ ¬ IsPisot α ∧
      ∃ c : ℝ, ∀ n : ℕ, 1 ≤ n → Int.fract (α ^ n) ∈ Set.Icc c (c + ε / α)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_7.lean, line 41.

Sources

• FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_7.lean at 2055e5ad

LeanBugeaud07.problem_10_7

TheoremBugeaud Collection of Conjectures and Open Questions: \(p\)-adic Littlewood Conjecture#

This is the \(p\)-adic analogue of the Littlewood conjecture, posed by de Mathan and Teulié. A liminf-based formulation also appears in the file FormalConjectures/Wikipedia/LittlewoodConjecture.lean as padic_littlewood_conjecture.

References: - [Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10. - [dMT04] de Mathan, Bernard, and Olivier Teulié. "Problèmes diophantiens simultanés." Monatshefte für Mathematik 143.3 (2004): 229-245. - [EK07] Einsiedler, Manfred, and Dmitry Kleinbock. "Measure rigidity and \(p\)-adic Littlewood-type problems." Compositio Mathematica 143.3 (2007): 689-702.

Quoted from FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_8.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 3 research or textbook statements: 1 open and 2 solved.

Bugeaud08.problem_10_8

Open: stated without proof.

Problem 10.8 (\(p\)-adic Littlewood conjecture). For every real number \(\xi\) and every prime number \(p\),

\[\inf_{q \ge 1} q \cdot \lVert q \xi \rVert \cdot |q|_p = 0,\]

where \(\lVert \cdot \rVert\) denotes the distance to the nearest integer and \(|\cdot|_p\) denotes the \(p\)-adic absolute value. Posed by de Mathan and Teulié [dMT04].

theorem problem_10_8 (ξ : ℝ) (p : ℕ) (hp : p.Prime) :
    sInf {x : ℝ | ∃ q : ℕ, 1 ≤ q ∧
      x = q * padicNorm p q * distToNearestInt (q * ξ)} = 0

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_8.lean, line 49.

Bugeaud08.problem_10_8.variants.quadratic

Solved: stated here without proof.

The quadratic case of Problem 10.8. de Mathan and Teulié [dMT04] solved the \(p\)-adic Littlewood conjecture for quadratic real numbers.

theorem problem_10_8.variants.quadratic (ξ : ℝ) (p : ℕ) (hp : p.Prime)
    (hξ : (minpoly ℚ ξ).natDegree = 2) :
    sInf {x : ℝ | ∃ q : ℕ, 1 ≤ q ∧
      x = q * padicNorm p q * distToNearestInt (q * ξ)} = 0

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_8.lean, line 59.

Bugeaud08.problem_10_8.variants.exceptional_set_dimH_zero

Solved: stated here without proof.

The exceptional set for Problem 10.8 has Hausdorff dimension zero (Einsiedler and Kleinbock [EK07].

theorem problem_10_8.variants.exceptional_set_dimH_zero (p : ℕ) (hp : p.Prime) :
    dimH {ξ : ℝ | Filter.atTop.liminf
      (fun q : ℕ ↦ q * padicNorm p q * distToNearestInt (q * ξ)) ≠ 0} = 0

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_8.lean, line 70.

Sources

• FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_8.lean at 2055e5ad

LeanBugeaud08.problem_10_8 · Bugeaud08.problem_10_8.variants.quadratic · Bugeaud08.problem_10_8.variants.exceptional_set_dimH_zero

TheoremBugeaud Collection of Conjectures and Open Questions: Mahler's Z-numbers#

See also FormalConjectures/Wikipedia/Mahler32.lean.

References: - [Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10. - [Mah68] Mahler, Kurt. "An unsolved problem on the powers of 3/2." Journal of the Australian Mathematical Society 8.2 (1968): 313-321. - [FLP95] Flatto, Leopold, Jeffrey C. Lagarias, and Andrew D. Pollington. "On the range of fractional parts \(\{\xi(p/q)^n\}\)." Acta Arithmetica 70.2 (1995): 125-147.

Quoted from FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_9.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 3 research or textbook statements: 1 open and 2 solved. It also has 1 test statement, counted here but not shown.

Bugeaud09.problem_10_9

Open: stated without proof.

Problem 10.9. There are no real numbers \(\xi\) such that \(0 \le \{\xi (3/2)^n\} < 1/2\) for every positive integer \(n\), i.e. no Z-number exists. Posed by Mahler [Mah68].

theorem problem_10_9 : type_of% Mahler32.mahler_conjecture

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_9.lean, line 44.

Bugeaud09.problem_10_9.variants.measure_zero

Solved: stated here without proof.

Mahler [Mah68] proved that the set of Z-numbers has Lebesgue measure zero.

theorem problem_10_9.variants.measure_zero :
    MeasureTheory.volume {ξ : ℝ | IsZNumber ξ} = 0

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_9.lean, line 64.

Bugeaud09.problem_10_9.variants.dimH_lt_one

Solved: stated here without proof.

Flatto, Lagarias, and Pollington [FLP95] proved that the set of Z-numbers has Hausdorff dimension strictly less than \(1\).

theorem problem_10_9.variants.dimH_lt_one :
    dimH {ξ : ℝ | IsZNumber ξ} < 1

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_9.lean, line 73.

Sources

• FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_9.lean at 2055e5ad

LeanBugeaud09.problem_10_9 · Bugeaud09.problem_10_9.variants.measure_zero · Bugeaud09.problem_10_9.variants.dimH_lt_one

TheoremBugeaud Collection of Conjectures and Open Questions: Automatic Expansions in Two Bases#

Problem 10.32 asks whether some irrational real number has automatic expansions in two multiplicatively independent bases. The answer is no. Adamczewski and Faverjon [AF20] proved it with the multivariate Mahler method, in a form that is stronger than the question asked: the base-\(b\) digit sequence may be \(k\)-automatic for an arbitrary \(k \ge 2\), not only for \(k = b\).

The definitions used here are in FormalConjecturesForMathlib: Nat.MultiplicativelyIndependent and Nat.MultiplicativelyIndependentFamily, AutomaticSequence.IsAutomatic, AutomaticSequence.IsAutomaticInBase and AutomaticSequence.IsBroadlyAutomaticInBase.

References: - AF20 Adamczewski, Boris, and Colin Faverjon. "Mahler's method in several variables and finite automata." arXiv:2012.08283 (2020). Appendix A, Conjectures A.2 and A.3, both proved there from Part (i) of Theorem 1.1. - [AS03] Allouche, Jean-Paul, and Jeffrey Shallit. "Automatic Sequences: Theory, Applications, Generalizations." Cambridge University Press, 2003. Chapter 13, Open Problems 7, p. 403, is the problem that Problem 10.32 modifies. - [Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10. - [Cob69] Cobham, Alan. "On the base-dependence of sets of numbers recognizable by finite automata." Mathematical Systems Theory 3 (1969): 186-192. - [LvdP82] Loxton, John H., and Alfred J. van der Poorten. "Arithmetic properties of the solutions of a class of functional equations." Journal für die reine und angewandte Mathematik 330 (1982): 159-172. Its transcendence method was the first attack on the problem; Nishioka later reported a gap in its main proof.

Quoted from FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_32.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 3 research or textbook statements: 3 solved.

Bugeaud32.adamczewski_faverjon

Solved: stated here without proof.

Adamczewski–Faverjon [AF20, Conjecture A.3], proved there from Part (i) of Theorem 1.1. Let \(b_1, \dots, b_r\) be multiplicatively independent positive integers, and for every \(i\) let \(\xi_i\) be a real number that is automatic in base \(b_i\). Then \(\xi_1, \dots, \xi_r\) are algebraically independent over \(\mathbb{Q}\), unless one of them is rational.

Two points of fidelity. The hypothesis is the joint multiplicative independence of \(b_1, \dots, b_r\) that [AF20] defines on p. 3 (no nonzero integer tuple \((n_i)\) has \(\prod_i b_i^{n_i} = 1\)), not the weaker pairwise condition; it is what the proof feeds to Part (i) of Theorem 1.1, via the multiplicative independence of \(1/b_1, \dots, 1/b_r\). Automaticity is the broad notion that the proof of Conjecture A.3 uses: the base-\(b_i\) digits of \(\xi_i\) are \(k\)-automatic for some \(k \ge 2\), which need not be \(b_i\).

theorem adamczewski_faverjon {r : ℕ} (b : Fin r → ℕ) (hb : ∀ i, 2 ≤ b i)
    (hind : Nat.MultiplicativelyIndependentFamily b)
    (ξ : Fin r → ℝ) (hauto : ∀ i, IsBroadlyAutomaticInBase (b i) (ξ i))
    (hirr : ∀ i, Irrational (ξ i)) :
    AlgebraicIndependent ℚ ξ

Category research solved; AMS 11 Number theory, 68 Computer science. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_32.lean, line 71.

Bugeaud32.problem_10_32.variants.strong

Proved here.

Problem 10.32, strong form. No irrational real number is automatic in two multiplicatively independent bases, in the broad sense that its digit sequence in each of the two bases is k-automatic for some k. This is [AF20, Conjecture A.2], with the broad notion of automaticity that its proof provides.

theorem problem_10_32.variants.strong (ξ : ℝ) (hξ : Irrational ξ) (b₁ b₂ : ℕ)
    (hb₁ : 2 ≤ b₁) (hb₂ : 2 ≤ b₂) (hind : Nat.MultiplicativelyIndependent b₁ b₂)
    (h₁ : IsBroadlyAutomaticInBase b₁ ξ) (h₂ : IsBroadlyAutomaticInBase b₂ ξ) : False

Category research solved; AMS 11 Number theory, 68 Computer science. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_32.lean, line 85.

Bugeaud32.problem_10_32

Proved here.

Problem 10.32. Is there an irrational real number whose expansions in two multiplicatively independent bases can both be generated by a finite automaton? The answer is no, by [AF20].

theorem problem_10_32 :
    ¬ ∃ ξ : ℝ, Irrational ξ ∧ ∃ b₁ b₂ : ℕ, 2 ≤ b₁ ∧ 2 ≤ b₂ ∧
      Nat.MultiplicativelyIndependent b₁ b₂ ∧
      IsAutomaticInBase b₁ ξ ∧ IsAutomaticInBase b₂ ξ

Category research solved; AMS 11 Number theory, 68 Computer science. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_32.lean, line 103.

Sources

• FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_32.lean at 2055e5ad
• AF20

LeanBugeaud32.adamczewski_faverjon · Bugeaud32.problem_10_32.variants.strong · Bugeaud32.problem_10_32

TheoremBugeaud Collection of Conjectures and Open Questions: Simultaneously Small Entropies#

A real number can be described by its continued fraction expansion and by its expansion in an integer base. Problem 10.53 asks for an irrational number for which both descriptions have small block complexity. Temur [Tem26] answered it, in the stronger form that asks for every base at once, by an explicit construction.

References: - [Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10. - Tem26 Temur, Faruk. "Simultaneously small continued fraction entropy and base \(b\) entropy." arXiv preprint arXiv:2609.16362 (2026). - [BBFKW10] Broderick, Ryan, Yann Bugeaud, Lior Fishman, Dmitry Kleinbock, and Barak Weiss. "Schmidt's game, fractals, and numbers normal to no base." Mathematical Research Letters 17.2 (2010): 307-321.

Quoted from FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_53.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 4 research or textbook statements: 4 solved.

Bugeaud53.problem_10_53

Solved: stated here without proof.

Problem 10.53. There is an irrational real number \(\xi\) such that \(E(\xi) < \log 2\) and \(E(\xi, b) < \log b\) for some integer \(b \ge 2\). Answered by Temur [Tem26].

theorem problem_10_53 :
    ∃ ξ : ℝ, Irrational ξ ∧ cfEntropy ξ < (Real.log 2 : EReal) ∧
      ∃ b : ℕ, 2 ≤ b ∧ baseEntropy b ξ < (Real.log b : EReal)

Category research solved; AMS 11 Number theory, 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_53.lean, line 50.

Bugeaud53.problem_10_53.variants.all_bases

Solved: stated here without proof.

Problem 10.53, in the stronger form that asks for every base at once: there is an irrational real number \(\xi\) such that \(E(\xi) < \log 2\) and \(E(\xi, b) < \log b\) for every integer \(b \ge 2\). Answered by Temur [Tem26].

theorem problem_10_53.variants.all_bases :
    ∃ ξ : ℝ, Irrational ξ ∧ cfEntropy ξ < (Real.log 2 : EReal) ∧
      ∀ b : ℕ, 2 ≤ b → baseEntropy b ξ < (Real.log b : EReal)

Category research solved; AMS 11 Number theory, 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_53.lean, line 61.

Bugeaud53.problem_10_53.variants.uncountable

Solved: stated here without proof.

There are uncountably many numbers as in Problem 10.53. This follows from a result of Broderick, Bugeaud, Fishman, Kleinbock and Weiss [BBFKW10] applied to the Gauss-Cantor set \(\{[0; 1, a_1, 1, a_2, \ldots] : a_j \in \{1, 2\}\}\), as observed in [Tem26].

theorem problem_10_53.variants.uncountable :
    ¬ {ξ : ℝ | Irrational ξ ∧ cfEntropy ξ < (Real.log 2 : EReal) ∧
      ∀ b : ℕ, 2 ≤ b → baseEntropy b ξ < (Real.log b : EReal)}.Countable

Category research solved; AMS 11 Number theory, 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_53.lean, line 72.

Bugeaud53.problem_10_53.variants.temur

Solved: stated here without proof.

Temur [Tem26], Theorem 1. There is an irrational \(\xi \in (0, 1)\) all of whose partial quotients are \(1\) or \(2\), such that

\[\lVert b^k \xi \rVert > 154^{-2^b} \quad (b \ge 2,\ k \ge 0),\]

where \(\lVert \cdot \rVert\) denotes the distance to the nearest integer. The bound on the partial quotients gives \(E(\xi) \le (\log 2) / 4\), and the displayed inequality forces the base \(b\) expansion of \(\xi\) to omit a block of zeros, which gives \(E(\xi, b) < \log b\) for every \(b \ge 2\). Temur's \(\xi\) is moreover computable.

theorem problem_10_53.variants.temur :
    ∃ ξ : ℝ, Irrational ξ ∧ ξ ∈ Set.Ioo (0 : ℝ) 1 ∧
      (∀ n : ℕ, partQuot ξ n = 1 ∨ partQuot ξ n = 2) ∧
      (∀ b : ℕ, 2 ≤ b → ∀ k : ℕ,
        (154 : ℝ) ^ (-(2 ^ b) : ℤ) < distToNearestInt ((b : ℝ) ^ k * ξ)) ∧
      cfEntropy ξ ≤ ((Real.log 2 / 4 : ℝ) : EReal) ∧
      ∀ b : ℕ, 2 ≤ b → baseEntropy b ξ < (Real.log b : EReal)

Category research solved; AMS 11 Number theory, 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_53.lean, line 87.

Sources

• FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_53.lean at 2055e5ad
• Tem26

LeanBugeaud53.problem_10_53 · Bugeaud53.problem_10_53.variants.all_bases · Bugeaud53.problem_10_53.variants.uncountable · Bugeaud53.problem_10_53.variants.temur

TheoremBugeaud Collection of Conjectures and Open Questions: Pisot orbits on the Cantor set#

Problem 10.61, proposed by Mendès France [MF67, Problème 1, p. 41]. For a Pisot number \(\alpha > 2\) put

\[C(\alpha) = \left\{ (\alpha - 1) \sum_{k \ge 1} \varepsilon_k \alpha^{-k} : \varepsilon_k \in \{0, 1\} \right\}.\]

The problem asks to prove that \((\xi \alpha^n)_{n \ge 1}\) is not uniformly distributed modulo one for any \(\xi \in C(\alpha)\). In the language of [MF67] this reads \(C(\alpha) \cap B(\alpha) = \emptyset\), where \(B(\alpha)\) is the set of \(\xi\) for which \((\xi \alpha^n)\) is uniformly distributed modulo one.

The problem is open. It is easy for an integer base and settled for two quadratic \(\alpha\); the general Pisot case is what remains. [Ste26] reduces it to a statement about shift-invariant measures of the full two-shift, and proves that every true instance admits a finite certificate, so the difficulty is uniformity in \(\alpha\) rather than any single \(\alpha\). The variants below state the criterion and the instances of [Ste26] that concern Problem 10.61 directly; the reduction itself is not stated here, since it needs the symbolic model.

Deleting the term \(n = 0\) does not change uniform distribution modulo one, so the statements indexed from \(n = 1\) agree with the ones of [Ste26], which are indexed from \(n = 0\). Where an orbit is confined away from an interval the stronger form, for every \(n \ge 0\), is stated.

References: - [Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10, Problem 10.61, p. 222. - [MF67] Mendès France, Michel. "Nombres normaux. Applications aux fonctions pseudo-aléatoires." Journal d'Analyse Mathématique 20 (1967): 1-56. - [Kok35] Koksma, Jurjen F. "Ein mengentheoretischer Satz über die Gleichverteilung modulo Eins." Compositio Mathematica 2 (1935): 250-258. - [Ste26] Stephan, Ralf. "Criteria for the non-equidistribution of \((\xi \alpha^n)\) on the Cantor set \(C(\alpha)\)." Preprint, 2026. https://doi.org/10.13140/RG.2.2.13923.52001

Quoted from FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_61.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 6 research or textbook statements: 1 open and 5 solved. It also has 2 test statements, counted here but not shown.

Bugeaud61.problem_10_61

Open: stated without proof.

Problem 10.61. Let \(\alpha > 2\) be a Pisot number. For every \(\xi \in C(\alpha)\) the sequence \((\xi \alpha^n)_{n \ge 1}\) is not uniformly distributed modulo one.

theorem problem_10_61 (α : ℝ) (hα : IsPisot α) (hα2 : 2 < α) :
    ∀ ξ ∈ pisotCantorSet α, ¬ IsEquidistributedModuloOne fun n : ℕ => ξ * α ^ (n + 1)

Category research open; AMS 11 Number theory, 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_61.lean, line 89.

Bugeaud61.problem_10_61.variants.almost_every

Solved: stated here without proof.

The hypothesis \(\xi \in C(\alpha)\) cannot be dropped: by Koksma's metric theorem [Kok35], for a fixed \(\alpha > 1\) the sequence \((\xi \alpha^n)_{n \ge 1}\) is uniformly distributed modulo one for Lebesgue-almost every \(\xi\). Problem 10.61 asks a null set of starting points to defeat an almost-everywhere law.

theorem problem_10_61.variants.almost_every (α : ℝ) (hα : 1 < α) :
    ∀ᵐ ξ ∂(MeasureTheory.volume : MeasureTheory.Measure ℝ),
      IsEquidistributedModuloOne fun n : ℕ => ξ * α ^ (n + 1)

Category research solved; AMS 11 Number theory, 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_61.lean, line 100.

Bugeaud61.problem_10_61.variants.covering_criterion

Solved: stated here; a Lean proof is at https://github.com/rwst/Pisot-Cantor-61/blob/a464f1cd3c8d14229a2f1d7881773987446d0df0/BB61/Criterion.lean#L230.

The covering criterion, [Ste26, Theorem C(i)], at a quadratic setup: \(\alpha > 1\) is a root of \(X^2 - aX - b\) whose conjugate \(\beta = a - \alpha\) is non-zero of modulus less than one. If the Route A exponent \(A(\alpha)\) formed from \(\alpha\) and \(\rho = |\beta|\) is below \(1\), then Problem 10.61 holds at \(\alpha\).

[Ste26] states the criterion for a Pisot number of any degree \(d \ge 2\), but proves it only in this degree-two case.

theorem problem_10_61.variants.covering_criterion {a b : ℤ} {α : ℝ}
    (hroot : α ^ 2 = a * α + b) (hα : 1 < α) (hβ : (a : ℝ) - α ≠ 0)
    (hconj : |(a : ℝ) - α| < 1) (hA : routeAExponent α |(a : ℝ) - α| < 1) :
    ∀ ξ ∈ pisotCantorSet α, ¬ IsEquidistributedModuloOne fun n : ℕ => ξ * α ^ (n + 1)

Category research solved; AMS 11 Number theory, 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_61.lean, line 117.

Bugeaud61.problem_10_61.variants.covering_criterion_range

Solved: stated here; a Lean proof is at https://github.com/rwst/Pisot-Cantor-61/blob/a464f1cd3c8d14229a2f1d7881773987446d0df0/BB61/RouteANormalForm.lean#L283.

The exact range of the covering criterion, [Ste26, Theorem C(ii)]: at a quadratic setup of norm \(-b\) one has \(A(\alpha) < 1\) if and only if \((\log_2 \alpha - 1)(\log_2(\alpha / |b|) - 1) > 1\), which for units reads \(\alpha > 4\). The criterion therefore never reaches the slice \(2 < \alpha \le 4\), and says nothing about a quadratic \(\alpha\) with \(A(\alpha) \ge 1\).

theorem problem_10_61.variants.covering_criterion_range {a b : ℤ} {α : ℝ}
    (hroot : α ^ 2 = a * α + b) (hα : 1 < α) (hconj : |(a : ℝ) - α| < 1) (hb : b ≠ 0) :
    routeAExponent α |(a : ℝ) - α| < 1 ↔
      1 < (Real.logb 2 α - 1) * (Real.logb 2 α - Real.logb 2 |(b : ℝ)| - 1)

Category research solved; AMS 11 Number theory, 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_61.lean, line 133.

Bugeaud61.problem_10_61.variants.two_add_sqrt_five

Solved: stated here; a Lean proof is at https://github.com/rwst/Pisot-Cantor-61/blob/a464f1cd3c8d14229a2f1d7881773987446d0df0/BB61/RouteA.lean#L163.

[Ste26, Theorem D] at \(\alpha = 2 + \sqrt 5\), the smallest \(\alpha\) the covering criterion reaches: Problem 10.61 holds there in the strong form. There is one open interval \(J \subseteq (0, 1)\), the same for every \(\xi \in C(\alpha)\) and every \(n \ge 0\), that \(\{\xi \alpha^n\}\) misses.

theorem problem_10_61.variants.two_add_sqrt_five :
    ∃ x r : ℝ, 0 < r ∧ Set.Ioo (x - r) (x + r) ⊆ Set.Ioo 0 1 ∧
      ∀ ξ ∈ pisotCantorSet (2 + Real.sqrt 5), ∀ n : ℕ,
        Int.fract (ξ * (2 + Real.sqrt 5) ^ n) ∉ Set.Ioo (x - r) (x + r)

Category research solved; AMS 11 Number theory, 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_61.lean, line 148.

Bugeaud61.problem_10_61.variants.two_add_sqrt_three

Solved: stated here; a Lean proof is at https://github.com/rwst/Pisot-Cantor-61/blob/a464f1cd3c8d14229a2f1d7881773987446d0df0/BB61/GapSqrtThree.lean#L298.

[Ste26, Theorem D] at \(\alpha = 2 + \sqrt 3\): Problem 10.61 holds there, by a confinement-gap certificate in exact \(\mathbb{Z}[\sqrt 3]\) arithmetic. This \(\alpha\) lies in the slice \(2 < \alpha \le 4\), which the covering criterion does not reach.

theorem problem_10_61.variants.two_add_sqrt_three :
    ∀ ξ ∈ pisotCantorSet (2 + Real.sqrt 3),
      ¬ IsEquidistributedModuloOne fun n : ℕ => ξ * (2 + Real.sqrt 3) ^ (n + 1)

Category research solved; AMS 11 Number theory, 37 Dynamical systems and ergodic theory. Declared in FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_61.lean, line 162.

Sources

• FormalConjectures/Books/BugeaudDistributionModuloOne/Problem10_61.lean at 2055e5ad
• https://doi.org/10.13140/RG.2.2.13923.52001

LeanBugeaud61.problem_10_61 · Bugeaud61.problem_10_61.variants.almost_every · Bugeaud61.problem_10_61.variants.covering_criterion · Bugeaud61.problem_10_61.variants.covering_criterion_range · Bugeaud61.problem_10_61.variants.two_add_sqrt_five · Bugeaud61.problem_10_61.variants.two_add_sqrt_three

TheoremEquidistributed Sequences#

Corollary 4.2 of Chapter 1 states that the sequence \((x^n), n = 1, 2, ... ,\) is equidistributed modulo 1 for almost all x > 1. And a little bit further down: "one does not know whether sequences such as \((e^n)\), \((π^n)\), or even \(((\frac 3 2)^n)\)" are equidistributed modulo 1 or not.

References: - Uniform Distribution of Sequences by L. Kuipers and H. Niederreiter, 1974 - Wikipedia - [Mat80] de Mathan, Bernard. "Numbers contravening a condition in density modulo 1." Acta Mathematica Hungarica 36.3-4 (1980): 237-241. - [Pol79] Pollington, Andrew Douglas. "On the density of sequence ${n_ {k}\xi} $." Illinois Journal of Mathematics 23.4 (1979): 511-515.

Quoted from FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean in Formal Conjectures (Google DeepMind) at commit 2055e5ad, Apache-2.0, as are the docstrings and Lean statements below.

The file states 5 research or textbook statements: 2 open, 2 solved and 1 textbook result. It also has 1 test statement and 1 API statement, counted here but not shown.

Equidistribution.isAccumulationPoint_exists_subsequence_tendsto

Textbook result, proved here.

If a point x is an accumulation point of a sequence s_0, s_1, ... then there is a subsequence of s that tends to x

theorem isAccumulationPoint_exists_subsequence_tendsto
    (x : ℝ) (s : ℕ → ℝ) (hx : IsAccumulationPoint x s) :
    ∃ (u : ℕ → ℕ), StrictMono u ∧ Filter.atTop.Tendsto (s ∘ u) (𝓝 x)

Category textbook; AMS 11 Number theory, 54 General topology. Declared in FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean, line 56.

Equidistribution.isEquidistributedModuloOne_three_halves_pow

Open: stated without proof.

The sequence (3/2)^n is equidistributed modulo 1.

theorem isEquidistributedModuloOne_three_halves_pow :
    IsEquidistributedModuloOne (fun n => (3 / 2 : ℝ)^n)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean, line 81.

Equidistribution.isEquidistributedModuloOne_transcendental_three_halves_pow

Solved: stated here without proof.

It is not true that for every transcendental number x the sequence x * (3 / 2) ^ n is equidistributed modulo 1. The sequence (3 / 2) ^ n is lacunary, so by the theorem of Pollington [Pol79] and de Mathan [Mat80] the set of real numbers x for which x * (3 / 2) ^ n is not even dense modulo 1 has Hausdorff dimension 1. This set is uncountable, so it contains transcendental numbers. Alternatively, an elementary nested-interval construction (see issue

5003) gives a Cantor set of x with Int.fract (x * (3 / 2) ^ (8 * j)) ∈ [0, 1 / 10] for all

j, which already rules out equidistribution for uncountably many, hence some transcendental, x. By Koksma's metric theorem (Kuipers–Niederreiter, Chapter 1, Section 4), the sequence x * (3 / 2) ^ n is equidistributed modulo 1 for almost all x.

theorem isEquidistributedModuloOne_transcendental_three_halves_pow :
    ¬ ∀ x : ℝ, Transcendental ℚ x →
      IsEquidistributedModuloOne (fun n ↦ x * (3 / 2 : ℝ) ^ n)

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean, line 95.

Equidistribution.isAccumulationPoint_three_halves_pow_infinite

Solved: stated here without proof.

The sequence (3/2)^n has infinitely many accumulation points modulo 1.

theorem isAccumulationPoint_three_halves_pow_infinite :
    {x | IsAccumulationPoint x (fun n => Int.fract <| (3 / 2 : ℝ)^n)}.Infinite

Category research solved; AMS 11 Number theory. Declared in FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean, line 104.

Equidistribution.isAccumulationPoint_three_halves_pow

Open: stated without proof.

Find an accumulation point of the sequence (3/2)^n modulo 1.

theorem isAccumulationPoint_three_halves_pow :
    IsAccumulationPoint isAccumulationPoint_three_halves_pow.answer
      (fun n => Int.fract <| (3 / 2 : ℝ)^n)

Category research open; AMS 11 Number theory. Declared in FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean, line 114.

Sources

• FormalConjectures/Books/UniformDistributionOfSequences/Equidistribution.lean at 2055e5ad
• Uniform Distribution of Sequences

LeanEquidistribution.isAccumulationPoint_exists_subsequence_tendsto · Equidistribution.isEquidistributedModuloOne_three_halves_pow · Equidistribution.isEquidistributedModuloOne_transcendental_three_halves_pow · Equidistribution.isAccumulationPoint_three_halves_pow_infinite · Equidistribution.isAccumulationPoint_three_halves_pow

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.