HEXAGONbeta

Hankel determinants and the length of finite Pierce expansions

Primarily AI-generated textHuman understanding: some partsmath.NT — Number Theorymath.CO — Combinatorics

Contributed by Jason Davies ↗

Version 1 / Oct 27, 2026 / CC BY 4.0

Abstract

For integers a>b>0a>b>0, let P(a,b)P(a,b) be the number of steps the iteration x↦a mod xx\mapsto a \bmod x takes to reach 00 from bb; it is the length of the Pierce expansion of b/ab/a. We prove P(a,b)≪εaβ∗+εP(a,b)\ll_\varepsilon a^{\beta_*+\varepsilon}, where β∗=(41301−382849)/137480=0.2941336553…\beta_*=(41301-3\sqrt{82849})/137480=0.2941336553\ldots, improving the exponent 1/3−2/1771/3-2/177 of Chase and Pandey. The tail of an orbit carries a sequence of positive integers, the Hankel determinants of a natural moment sequence, and these are small where the drops of the orbit are small. Grouping orbit states by such integers places the quotient differences of each group on curves of bounded degree, whose integer points we count with the uniform bounds of Castryck, Cluckers, Dittmann and Nguyen. The resulting exponent approaches 5/175/17 when these curves have large degree relative to the logarithmic size of the box. We raise the degree by adjoining further integer invariants, by an effective Hilbert irreducibility sieve, and by an exact identity for the direction of the curvature vector, and come within 1.61⋅10−51.61\cdot10^{-5} of 5/175/17. We also give an elementary proof of the exponent 3/10+ε3/10+\varepsilon and a bound for orbits whose quotient increments rarely rise. All results are formalised in Lean 4 with Mathlib. Shallit's conjectured O((log⁡a)2)O((\log a)^2) bound remains open.

Provenance statement

This work was produced by an AI-driven research process. The human author initiated the investigation and directed the AI systems throughout, but wrote no part of the manuscript or of the Lean code. GPT-6-Astra (OpenAI), used through Codex, found the results and the key steps of their proofs. GPT-6-Astra and Claude Opus 5.5 (Anthropic), used through Claude Code, developed the presentation, the Lean 4 formalisation and the writing, and reviewed and revised the manuscript. Every theorem in the paper is formalised in Lean 4 with Mathlib and machine-checked relative to the standard axioms propext, Classical.choice and Quot.sound. The development is registered in the Palomar registry as PALOMAR-2026-10-27-000017 (version 1, commit 6da6511). The conditional refinement assumes two published analytic estimates as explicit hypotheses. These automated checks are not independent human peer review. Full details are in the paper's section "Declaration of AI-generated research and authorship".

Formalizations

Tools used

OpenAI
CodexVersion GPT-6-Astra
Anthropic
Claude CodeVersion Claude Opus 5.5
Lean
LeanVersion 4

References

  1. O. Baraskar and I. Vukusic, Bounds for sets of remainders , arXiv:2508.20853 (https://arxiv.org/abs/2508.20853) (2025).arXiv
  2. R. de la Bretèche and G. Tenenbaum, Note on the mean value of the Erdős--Hooley Delta-function , Acta Arith.\ 219 (2025), no. 4, 379--394, doi:10.4064/aa250107-13-2 (https://doi.org/10.4064/aa250107-13-2).DOI
  3. W. Castryck, R. Cluckers, P. Dittmann and K. H. Nguyen, The dimension growth conjecture, polynomial in the degree and without logarithmic factors , Algebra Number Theory 14 (2020), no. 8, 2261--2294, doi:10.2140/ant.2020.14.2261 (https://doi.org/10.2140/ant.2020.14.2261).DOI
  4. R. Cluckers, P. Dèbes, Y. I. Hendel, K. H. Nguyen and F. Vermeulen, Improvements on dimension growth results and effective Hilbert's irreducibility theorem , Forum Math.\ Sigma 13 (2025), e153, doi:10.1017/fms.2025.10096 (https://doi.org/10.1017/fms.2025.10096).DOI
  5. Z. Chase and M. Pandey, On the length of Pierce expansions , arXiv:2211.08374 (https://arxiv.org/abs/2211.08374) (2022).arXiv
  6. P. Erdős and J. O. Shallit, New bounds on the length of finite Pierce and Engel series , J.\ Théor.\ Nombres Bordeaux 3 (1991), no. 1, 43--53, doi:10.5802/jtnb.41 (https://doi.org/10.5802/jtnb.41).DOI
  7. J. Franke, Yu. I. Manin and Yu. Tschinkel, Rational points of bounded height on Fano varieties , Invent.\ Math.\ 95 (1989), 421--435, doi:10.1007/BF01393904 (https://doi.org/10.1007/BF01393904).DOI
  8. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language , in: Automated Deduction -- CADE 28, Lecture Notes in Comput.\ Sci.\ 12699 , Springer, 2021, 625--635, doi:10.1007/978-3-030-79876-5_37 (https://doi.org/10.1007/978-3-030-79876-5_37).DOI
  9. The mathlib Community, The Lean mathematical library , in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), 367--381, doi:10.1145/3372885.3373824 (https://doi.org/10.1145/3372885.3373824).DOI
  10. M. Nair and G. Tenenbaum, Short sums of certain arithmetic functions , Acta Math.\ 180 (1998), 119--144, doi:10.1007/BF02392880 (https://doi.org/10.1007/BF02392880).DOI
Show all 15 referencesShow fewer references
  1. OpenAI, openai/math , https://github.com/openai/math.link
  2. J. O. Shallit, A discrete iteration related to Pierce expansions , Open Problem Garden, https://www.openproblemgarden.org/op/a_discrete_iteration_related_to_pierce_expansions.link
  3. T. A. Pierce, On an algorithm and its use in approximating roots of algebraic equations , Amer.\ Math.\ Monthly 36 (1929), no. 10, 523--525, doi:10.1080/ 00029890.1929.11987017 (https://doi.org/10.1080/00029890.1929.11987017).DOI
  4. J. O. Shallit, Metric theory of Pierce expansions , Fibonacci Quart.\ 24 (1986), no. 1, 22--40, doi:10.1080/00150517.1986.12429786 (https://doi.org/10.1080/00150517.1986.12429786).DOI
  5. J. O. Shallit, Talks , https://cs.uwaterloo.ca/~shallit/talks.html (accessed October 2026).link

Version history

  1. v1Submitted by Jason DaviesInitial depositCurrentOct 27, 2026