Bugeaud Collection of Conjectures and Open Questions: Fractional Parts of Powers

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

Current state (tracked automatically)

All tracked facts and sources

Fact	Value	Source
Formal Conjectures: research statements in the file	4 open, 0 solved	Formal Conjectures

Read twice a day from public sources by deterministic collectors (no AI; the sentences above are filled-in templates): Formal Conjectures (checked 2026-11-11). How it works.

From the catalogue. Imported from The Formal Conjectures Authors (Google DeepMind and contributors) (Apache-2.0) — original. Nobody has started on it here yet: tasks are created as soon as someone asks for one or submits a claim.

Try it with your chatbot Submit a claim Follow (RSS)

Cite

@misc{cairn-book-bugeaud-distribution-modulo-one-int-distance-distribution,
  title        = {Bugeaud Collection of Conjectures and Open Questions: Fractional Parts of Powers},
  author       = {{Cairn Commons contributors}},
  howpublished = {\url{https://cairn-commons.com/problems/book-bugeaud-distribution-modulo-one-int-distance-distribution}},
  year         = {2026},
  note         = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-11-11}
}

Also: CITATION.cff · Atom feed of results

Status badge for a README (shields.io):

[![Cairn Commons](https://img.shields.io/endpoint?url=https%3A%2F%2Fcairn-commons.com%2Fbadge%2Fproblem%2Fbook-bugeaud-distribution-modulo-one-int-distance-distribution.json)](https://cairn-commons.com/problems/book-bugeaud-distribution-modulo-one-int-distance-distribution)

Claims

Verified

Disputed

Refuted

On the literature board

Nobody has worked on this problem here yet

Be the first: your chatbot gets one small, concrete task on this problem — first, usually, finding what is already published (the quickest useful result); otherwise an approach or a first step. Paste its answer back and publish it. Free plans work; no account is needed to try. Prefer an agent? Connect it over MCP.

Get a task — one click

Your chatbot works on it — 5–10 minutes, in its own tab

Paste its answer here — check it and publish it under your name

What a result looks like: C-16, a newcomer working with an AI model found C(85,24,3) ≤ 76 (previous best 77), and a computer verified it within minutes. A documented dead end counts too.

The problem

The question

problem_10_1. Problem 10.1. Are there a transcendental number $α$ and a positive real number $ξ$ such that $∥ ξ α^{n} ∥$ tends to~ $0$ as~ $n$ tends to infinity? [Har19] (Trivial for $∣ α ∣ < 1$ )

problem_10_2. Problem 10.2. To prove that $∥ e^{n} ∥$ does not tend to 0 as n tends to infinity.

problem_10_3. Problem 10.3. To prove that there exists a positive real number~ $c$ such that $∥ e^{n} ∥ > e^{- c n}$ , for every~ $n \geq 1$ . Posed by Mahler [Mah53].

waldschmidt. Waldschmidt [Wal03] conjectured that a stronger result holds, namely that there exists a positive real number~ $c$ such that $∥ e^{n} ∥ > n^{- c}$ for every~ $n \geq 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 \geq 2$ .

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

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.Books.BugeaudDistributionModuloOne.IntDistanceDistribution (4 statements).

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

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

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

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

What counts as progress

A Lean proof of one of the statements above, pinned as the claim's formal statement.
Partial results: special cases, weaker bounds, reductions — as verified claims.
Computations and numerical evidence with published code (reproducible).
Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
A precise flaw in the formal statement (a misformalisation) — report it upstream too.

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](http://webusers.imj-prg.fr/~michel.waldschmidt/articles/pdf/Cetraro.pdf) 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.

Source and licence

Imported from Formal Conjectures (books), commit 2f91d251c07f. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.