Research project · Number theory · Computer-assisted proof

Infinitely many composites, for every ξ

and

Pick any real number ξ > 0. Multiply it by 7/5 again and again, and keep only the integer part each time. The resulting sequence always contains infinitely many composite numbers — and so do the ones for 5/2 and 5/3. The proof supposes that from some point on no term is divisible by any of a few small primes, traps every such sequence in a finite graph, and prunes that graph until nothing is left.

Read the paper Try any ξ Watch the explainers

Yuri Odagiri · 2026 · DOI 10.5281/zenodo.22997709 · GitHub

2 composite, divisible by this primeprimecomposite, other factors

01The result

Three theorems about integer parts of powers

In 1967 Forman and Shapiro proved that ⌊(3/2)n⌋ and ⌊(4/3)n⌋ contain infinitely many composite numbers, by arguments that also work after multiplying by any ξ > 0; Dubickas and Novikas added 5/4. For 7/5 they treated the nearest integers, and for 5/2 a shifted sequence; for 5/3, Novikas’s thesis treats the nearest integers. This work proves the statements for the plain integer parts. What was known, and what is new →

Theorem 1 (i)7/5

for infinitely many n, whatever ξ > 0 is

4290 = 2351113

  • One-step graph certificate, four stages
  • Lean: checked by the kernel

Theorem 1 (ii)5/2

for infinitely many n, whatever ξ > 0 is

40112098026 = 23711131719232931

  • Word-labelled certificate, ten stages (the prime 5 is not needed)
  • Lean: kernel-checked soundness, native_decide evaluation

Theorem 1 (iii)5/3

for infinitely many n, whatever ξ > 0 is

1484147626962 = 2371113171923293137

  • Word-labelled certificate contracted in both directions, ten stages (the prime 5 is not needed)
  • Lean: kernel-checked soundness, native_decide evaluation

Corollary 2For every ξ > 0, all three of ⌊ξ(7/5)n⌋, ⌊ξ(5/2)n⌋ and ⌊ξ(5/3)n⌋ contain infinitely many composite terms: a term larger than 37 that shares a factor with its modulus is composite, and the terms grow without bound.

Theorem 3For 7/5 there is even an explicit waiting time: a composite term within 428 + 12L(P) steps.

02In context

What was known, and what is new

Composite numbers in sequences like these have been studied since 1967. On the left, the earlier results this work builds on or is compared with; on the right, what this paper adds.

Known before

  1. 1967
    Forman & Shapiro — ⌊(3/2)n⌋ and ⌊(4/3)n⌋ contain infinitely many composite numbers; the argument also works after multiplying by any ξ > 0.
  2. 2005
    Dubickas & Novikas — Explicit sets of primes that divide infinitely many terms for every ξ: for 3/2, 4/3 and 5/4, for the nearest integers to ξ(7/5)n, and for ⌊ξ(5/2)n⌋ − 1. They also settled the integer bases 2 to 6. Their paper already contains the fact that this work prunes with: the carries of a true sequence are never periodic.
  3. 2006
    Dubickas — Named such a set of primes unavoidable. Among integer bases, none exists for 5, nor for any b ≥ 3 with b − 1 not squarefree; he conjectured that none exists for any integer base other than 2, 3, 4 and 6.
  4. 2009
    Dubickas — A return theorem: a sequence given by a suitable integer recurrence repeats periodically modulo every q coprime to one fixed coefficient. So it keeps returning to multiples of each of its large prime terms; in particular, a periodic pattern of digits forces composite terms.
  5. 2012
    Novikas (thesis) — States that, for every ξ > 0, the nearest integers to ξ(5/3)n include infinitely many terms divisible by 2 or 3.
  6. 2022
    Dubickas & Jonuška — For base 7, their theorem implies that for every finite set of primes some ξ makes no term divisible by any of them: no unavoidable set exists.
  7. 2026
    Stephan (preprint) — ⌊ξ7n⌋ contains infinitely many composite numbers for every ξ > 0, the smallest integer base that was open. The proof uses a finite graph certificate closely related to the one here, checked in Lean. Compared below.

New in this paper

  • Theorem 1. For the plain integer parts ⌊ξ(7/5)n⌋, ⌊ξ(5/2)n⌋ and ⌊ξ(5/3)n⌋: fixed sets of primes (unavoidable sets) that divide infinitely many terms for every ξ, and hence infinitely many composite terms (Corollary 2). Before, 7/5 and 5/3 had been treated only with nearest integers, and 5/2 only with a shift.
  • The certificates. Finite graphs of residues and fractional-part cells for a rational base, pruned with the nonperiodicity of the carries; and the word-labelled method, which contracts paths exactly and checks the primes at every intermediate term. For 5/3, chains with only one way in are contracted too.
  • Theorem 3. An explicit waiting time for 7/5.
  • The method itself. A normal form, two obstructions, and a lower bound for the extra primes a certificate needs. For 5/3: membership in the certifiable class, and an obstruction showing that the primes up to 23 are not enough.
  • Further results. Recurrent carries force composites (Theorem 46, a return argument in the spirit of Dubickas’s 2009 theorem); checks up to a height for 6/5 and 9/7; a halting problem for (6t+3)/(6t+1).
  • Verification. Two independently written implementations, compared element by element, and a Lean formalization of all three parts of Theorem 1 and Corollary 2.

03Try it

Choose your own ξ

Type any positive number. The page computes the terms exactly, and marks each composite term with the smallest certificate prime that divides it. No list of terms can prove the theorem — that is what the finite certificate is for — but you can watch the marked terms keep coming.

    3 composite, divisible by this certificate primecomposite, no certificate primeprime

    04The method

    Trap the exceptions in a finite graph, then prune it to nothing

    Suppose, for contradiction, that from some point on no term of ⌊ξ(7/5)n⌋ is divisible by 2, 3, 5, 11 or 13. Call the terms from that point on an exceptional tail. (Its terms need not be prime: 323 = 17 × 19 is divisible by none of the five.) The proof shows, in three steps, that no exceptional tail exists.

    1

    Carries are small

    Write Qn for the n-th term. The carry cn = 5Qn+1 − 7Qn is always one of the eleven integers −4, …, 6. So an exceptional tail obeys finitely many local rules: the residues modulo 4290, the fractional parts and the carries fit together in only finitely many ways.

    For ξ = π: the terms 3, 4, 6, 8, 12, 16, 23 and their carries.
    2

    A finite graph traps every exceptional tail

    New for rational basesCompare: Stephan, base 7

    A state records the residue of a term modulo 4290 and which of K equal cells contains its fractional part; an edge is a legal step with its carry. Every exceptional tail becomes an infinite walk in this finite graph — for 7/5 it starts with 960 × 32 = 30,720 states.

    An exceptional tail, if there were one, would walk forever (yellow). Pruning the components that cannot host a true sequence leaves nothing.
    3

    Prune until nothing is left

    Nonperiodicity lemma: Dubickas–Novikas 2005Pruning certificate: new

    An infinite walk eventually stays inside one strongly connected component. If every walk there would make the carries periodic — impossible for a true sequence, by an elementary nonperiodicity lemma already in Dubickas–Novikas (2005) — the component is removed. What remains is refined, each cell split into four, and the test is repeated. For 7/5, the fourth stage keeps nothing: no exceptional tail exists.

    The four stages for 7/5 (Table 1 of the paper). Each whole bar is all the vertices of a stage, and its yellow left end is the single component that is kept; everything else is removed. Every kept vertex is then split into four finer cells, so the next stage has exactly four times as many vertices. At K = 2048 nothing is kept.

    Five halves: words on the edges

    New

    For ⌊ξ(5/2)n⌋ a direct graph over all ten primes would have 30,656,102,400 states. The word-labelled method starts instead from four vertices and just three carries, −1, 1 and 3 (a term not divisible by 2 is odd, and the carry after an odd term is odd), lets each edge carry a whole word of carries, contracts deterministic paths exactly, and adds one prime at a time — checking the remainder at every intermediate term of every word. The largest graph it builds has 2,856,938 vertices, and its output is empty. The same method also gives a second proof for 7/5.

    Input vertices at the ten stages for 5/2 (Table 6, logarithmic scale), with the prime added at each stage.

    Five thirds: contracting in both directions

    New

    For ⌊ξ(5/3)n⌋, a term not divisible by 2 or 3 leaves just three carries, −2, 2 and 4, and three cells are enough to start. But with forward contraction alone, the graph for the last prime, 37, would have 313,651,296 vertices. So the certificate for 5/3 also contracts chains of vertices that have only one way in: a walk through such a vertex must have arrived along that one arrow, so the words can be joined backwards, just as corridors are joined forwards. Contracting in both directions keeps the largest graph at 21,077,909 vertices. At the prime 37, all 14,920 components with loops pass the test, and the output is empty.

    Input vertices at the ten stages for 5/3 (Tables 17 and 18, logarithmic scale). Grey: forward contraction only; the grey bar at 37 was counted, not built. Blue: contracting in both directions, as in the certificate.

    A close relative: Stephan’s proof for base 7

    In August 2026, shortly before this paper, Ralf Stephan posted a preprint proving that ⌊ξ7n⌋ contains infinitely many composite numbers for every ξ > 0. His method shares several ingredients with this one: a finite graph of residues (modulo 2 · 3 · 5 · … · 31), built by adding one prime at a time; rank functions that a checker verifies in place of proving graph algorithms correct; and a Lean verification that runs the finite computation with native_decide. The difference is what happens to periodic behaviour.

    AspectStephan (2026) · base 7This paper · 7/5, 5/2 and 5/3
    States of the graphresiduesresidues and fractional-part cells; every true sequence gives a walk, but a walk need not be a sequence
    Parts in which every walk is periodickept: periodic digit patterns really occur, with no term divisible by a prime up to 31deleted: the carries of a true sequence are never periodic
    What is lefta core of 371,702 statesnothing
    Why composites followDubickas’s return theorem (2009): a periodic digit pattern forces composite termsa fixed set of primes divides infinitely many terms
    A fixed set of primes that works for every ξnone exists for base 7 (Dubickas–Jonuška 2022){2, 3, 5, 11, 13} for 7/5, {2, 3, 7, 11, …, 31} for 5/2, and {2, 3, 7, 11, …, 37} for 5/3
    Leanevery numbered statement; the finite computation by native_decideTheorem 1 and Corollary 2; the 7/5 one-step certificate in the kernel, the word-labelled runs by native_decide

    Stephan’s computation is not used in any proof of this paper; the paper’s introduction compares the two methods. Stephan’s preprint · its Lean files

    05Waiting time

    How long until the next composite?

    New in this paper

    Theorem 3 If P = ⌊ξ⌋ > 13, then some 0 ≤ n ≤ 428 + 12L(P) has gcd(⌊ξ(7/5)n⌋, 4290) > 1, and that term is composite.

    Applied from any term onward, it says that a composite term arrives within 428 + 12L(QN) steps of any term QN > 13: the gaps between composite terms grow at most like the logarithm of the terms. The proof builds one more graph — 491,520 states and 891,990 arrows, whose blocks can be stacked in 65 levels — and adds up, exactly, the time a walk can spend at each level.

    Yellow: the proved bound. Blue: the longest wait found by an exact search over every ξ with 14 ≤ ⌊ξ⌋ < 107 — 13 steps, first at ⌊ξ⌋ = 8,887,499, where the bound is 548. The search was run for the explainer video and is not part of the paper.

    06Reach and limits

    What the method can and cannot do

    New in this paper

    The paper also proves theorems about the certificate method itself, for a general base a/b.

    A normal form

    With its operations fixed precisely, a finite certificate exists exactly when, for some cell count and some finite set of primes not dividing 2ab, every cyclic component of one explicit graph passes the phase test. Contraction, prime powers and the primes dividing 2ab never enlarge what can be certified.

    Large numerators

    The method can never terminate when a ≥ 2 rad M. With the primes of 4290, for example, it certifies none of the fractions (14k+1)/(10k+1) with k ≥ 613, although they approach 7/5.

    A budget of primes

    Two carry words can combine into pseudo-orbits that no graph can exclude, unless extra primes are added. Their product R must satisfy

    5/2 with no primes except 2 and 5: running backward, the words U = (1) and V = (3, 1) map I = [1/3, 17/21] into two disjoint parts of itself. Every infinite choice of words gives nested intervals that never become empty — a pseudo-orbit (outlined).

    Obstructions, not counterexamples

    These results say that a fixed procedure does not terminate. They are not counterexamples to any arithmetic statement, and they do not assert that any base has only finitely many composite terms. They map out where finite certificates of this kind can and cannot reach.

    Five thirds, from both sides

    New

    The certificate for 5/3 shows that it belongs to the certifiable class of the normal form, without building that graph’s 413,857,382,400 vertices. In the other direction, two carry words of lengths 119 and 134 give pseudo-orbits that survive every graph built from the primes up to 23, so any certificate of this kind for 5/3 needs a prime of at least 29. Whether 29 is enough is not known.

    07Further results and open problems

    Beyond the main theorems

    Recurrent carries

    NewIn the spirit of Dubickas 2009

    For any coprime a > b ≥ 2: if the carry sequence of an orbit has a recurrent tail, the orbit has infinitely many composite terms (Theorem 46).

    Checked up to a height

    New

    If 6 < ⌊ξ⌋ ≤ 540, one of the first 41 terms of ⌊ξ(6/5)j⌋ is composite; if 9 < ⌊ξ⌋ ≤ 718, one of the first 19 terms of ⌊ξ(9/7)j⌋ is (Theorem 47).

    A halting problem

    New

    For the family (6t+3)/(6t+1), which contains 9/7, the statement for all coefficients reduces to whether an explicit integer program always halts (Theorem 58).

    Five open problems

    1. Further bases and infinite families. Which other rational bases admit finite certificates, and can one certificate cover an infinite family? Appendix F adds 5/3 to the bases known to be certifiable.
    2. Finite height versus all coefficients. Extend the checks for 6/5 and 9/7 beyond the stated heights.
    3. Recurrence. Can a tail of prime terms have non-recurrent carries?
    4. Additional operations. Do sharper operations certify more bases? Does the halting program always halt?
    5. Minimality and subsequences. Are the prime sets minimal? For 5/3 it is known only that some prime of at least 29 is needed. What happens along arithmetic progressions of indices, and how rare are prime terms?

    08Verification

    Checked twice: by independent programs, and by Lean

    Two implementations

    Every finite computation was carried out by two implementations whose scientific cores were written separately, and their complete outputs were compared element by element — not by counts, and not by hashes.

    • One-step (Tables 1–3): Kosaraju (A) against Tarjan (B), with B written from the specification without reading A and its outputs fixed before the comparison. They agree on 97,772 vertices, 168,474 labelled edges and 94,006 components, and B’s checker rejects 13 deliberately corrupted certificates.
    • Word-labelled (Tables 4, 6, 7): all 29 pairs of graph files agree element by element.
    • 5/3 (Table 17): the program that first computed the certificate, which checks every lifted edge and every contraction as it runs, against implementation B extended with backward passes, written from the lemma without reading that program. All 20 graphs agree byte for byte: 35,289,089 vertices, 48,786,290 edges and 1,245,585,922 letters.

    A Lean 4 formalization

    • 7/5: the four-stage certificate is checked inside the Lean kernel. The final theorems depend only on the standard axioms propext, Classical.choice and Quot.sound, as reported in the paper.
    • 5/2: the pipeline runs inside Lean and its soundness theorem is kernel-checked; the finite run uses native_decide, which adds trust in Lean’s compiler and native evaluation — never in Python or C++ success flags, graph files or hashes.
    • 5/3: the in-direction contraction is proved in its original direction, and a precompiled copy of the pipeline with backward passes (WordExec) is evaluated by native_decide — 657 s and 12.7 GiB on the recorded machine. The trust is of the same kind as for 5/2; the independent audit predates this addition and does not cover it.
    • Outside the formalization: Theorem 3, Sections 6–8 and 10, Appendices B–E, Corollaries 77 and 78 of Appendix F, and the table counts. There the evidence is the written proofs and the A/B comparisons.

    Theorem 1 (i), as stated in Lean

    theorem floor_seven_fifths_visits (ξ : ℝ) (hξ : 0 < ξ) (N : ℕ) :
    ∃ n : ℕ, max N 1 ≤ n ∧ 1 < Int.gcd ⌊ξ * (7 / 5 : ℝ) ^ n⌋ 4290 := by
  exact finite_success_visits 7 5 4290 (by decide) (by decide) (by decide)
    (by decide) mainFiniteSuccess ξ hξ N

    supplement/lean/MathPaper/Main.lean

    Reproduce it

    # file identity: the package manifest and the file hashes
python3 -B reproduce.py verify
# preflight: unit checks and selected small computations
python3 -B reproduce.py check --output /tmp/floor-paper-check
# every finite result, with the two implementations compared element by element
python3 -B reproduce.py recompute --output /tmp/floor-paper-full

    Each command runs under fixed limits: 600 s and 8 GiB per command, and 1800 s in all for check, 3600 s for recompute, which includes the 5/3 computation and writes about 10 GB of graph data. The Lean proofs are built separately with Lean 4.29.1 and a pinned Mathlib. See REPRODUCE.md, COMPUTATION.md and FORMALIZATION.md.

    09Explainer videos

    Animated explainers, narrated

    Four animations walk through the paper, each in English and Japanese; a longer Japanese explainer covers the basics at high-school level.

    10Paper, code, citation

    Read, reproduce, cite

    Paper (English)PDF Paper (Japanese)PDF DOI10.5281/zenodo.22997709 Source codeGitHub Lean formalizationsupplement/lean Finite computationsimplementations A and B

    Cite

    Yuri Odagiri. Finite graph certificates for composite terms in rational floor sequences. 2026. doi:10.5281/zenodo.22997709

    @misc{odagiri2026finite,
  author    = {Odagiri, Yuri},
  title     = {Finite graph certificates for composite terms in rational floor sequences},
  year      = {2026},
  publisher = {Zenodo},
  doi       = {10.5281/zenodo.22997709},
  url       = {https://doi.org/10.5281/zenodo.22997709}
}

    11Provenance

    How this work was made

    The paper’s acknowledgments describe its provenance in detail. It grew out of the author’s question whether every Mills number is irrational — a question the paper does not resolve.

    After that initial conjecture, the mathematical development, the computation programs, the exposition and the Lean formalization were all carried out by AI systems. The internal reviews were automated critiques, not independent review by human mathematicians. The author has personally confirmed that the Lean proofs are accepted by Lean, and asks readers to assess the arguments, the reproducible computations and the formal proofs themselves.

    For version 3.0.0, which adds 5/3, the author proposed reversing the search: looking for bases that admit a certificate, instead of trying to prove preselected ones. The search and the certificate for 5/3 were produced by GPT-6 Pro in ChatGPT; the second implementation, the Lean formalization and the integration into the paper were carried out by AI through Claude Code.

    The explainer animations and this page were also produced with AI assistance.

    Read the full disclosure in the paper →