HEXAGONbeta

The Euclidean algorithm is not optimal among uniform processes

Primarily AI-generated textHuman understanding: some partsmath.LO — Logicmath.NT — Number Theorycs.CC — Computational Complexitycs.LO — Logic in Computer Science

Contributed by Jason Davies ↗

Version 1 / Oct 29, 2026 / CC BY 4.0

Abstract

Reusing a stored Euclidean prefix, we show that every pair a≥ba\geq b has a derivation of gcd⁡(a,b)\gcd(a,b) from a,ba,b with O(log⁡a/log⁡log⁡a)O(\log a/\log\log a) applications of the remainder function alone; Euclid's algorithm needs order log⁡a\log a in the worst case. These derivations bound the intrinsic complexity of gcd and coprimeness by the same order, refuting Moschovakis's conjectured logarithmic lower bounds for uniform processes; by his best-uniform-process theorem, a single uniform process attains this bound. The Main Conjecture for algorithms remains open. We also prove an Ω(log⁡log⁡a)\Omega(\log\log a) lower bound on this complexity for almost all coprime pairs and give, for each ε>0\varepsilon>0, a nondeterministic register program computing gcd that, on every input a≥b≥1a\geq b\geq1, has a successful computation using at most εlog⁡a+O(1)\varepsilon\log a+O(1) remainder calls. The upper bound also answers negatively an open problem of van den Dries and Moschovakis on the closure depth of the gcd. The main bounds and the refutations are formalised in Lean 4; the best-uniform-process theorem is cited.

Provenance statement

The principal result was identified by GPT-6-Astra (OpenAI), used through Codex, during a broader investigation initiated by the author. The author then directed GPT-6-Astra and Claude Opus 5.5 (Anthropic), used through Claude Code, to develop the results, formalise them in Lean 4 and write the manuscript; both systems also reviewed and revised it over several rounds. The author directed the work and wrote no part of the text or the Lean code. The main bounds and the refutations are formalised in Lean 4 with mathlib, and Palomar's comparator confirms that the 22 compared statements are proved, rechecked by two independent proof checkers, using only Lean's standard axioms. The author has checked the arguments and takes full responsibility for the content.

Formalizations

Tools used

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

References

  1. Nader H. Bshouty. Euclidean GCD algorithm is not optimal . Research Report 1989-376-38, Department of Computer Science, University of Calgary, December 1989. doi:10.11575/ PRISM/30475 (https://doi.org/10.11575/PRISM/30475).DOI
  2. Benny Chor and Oded Goldreich. An improved parallel algorithm for integer GCD. Algorithmica 5(1--4):1--10, 1990. doi:10.1007/BF01840374 (https://doi.org/10.1007/BF01840374).DOI
  3. Leonardo de Moura and Sebastian Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction -- CADE 28 , Lecture Notes in Computer Science, vol. 12699, pp. 625--635. Springer, 2021. doi:10.1007/978-3-030-79876-5_37 (https://doi.org/10.1007/978-3-030-79876-5_37).DOI
  4. Ravindran Kannan, Gary Miller and Larry Rudolph. Sublinear parallel algorithm for computing the greatest common divisor of two integers. SIAM Journal on Computing 16(1):7--16, 1987. doi:10.1137/0216002 (https://doi.org/10.1137/0216002).DOI
  5. Donald E. Knuth. The Art of Computer Programming, Vol. 2: Seminumerical Algorithms , 3rd ed. Addison-Wesley, Reading, MA, 1997.
  6. Yishay Mansour, Baruch Schieber and Prasoon Tiwari. A lower bound for integer greatest common divisor computations. Journal of the ACM 38(2):453--471, 1991. doi:10.1145/103516.103522 (https://doi.org/10.1145/103516.103522).DOI
  7. Yishay Mansour, Baruch Schieber and Prasoon Tiwari. Lower bounds for computations with the floor operation. SIAM Journal on Computing 20(2):315--327, 1991. doi:10.1137/0220020 (https://doi.org/10.1137/0220020).DOI
  8. The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020) , pp. 367--381. ACM, 2020. doi:10.1145/3372885.3373824 (https://doi.org/10.1145/3372885.3373824).DOI
  9. Yiannis N. Moschovakis. Absolute lower bounds for uniform processes . Unpublished lecture notes (first draft), January 25, 2012. https://www.math.ucla.edu/~ynm/nadalb.pdf.link
  10. Yiannis N. Moschovakis. Abstract Recursion and Intrinsic Complexity . Lecture Notes in Logic, vol. 48. Cambridge University Press and Association for Symbolic Logic, 2019. doi:10.1017/9781108234238 (https://doi.org/10.1017/9781108234238).DOI
Show all 14 referencesShow fewer references
  1. Palomar registry. Entry PALOMAR-2026-10-23-000012, version 2, for commit 2548681 of https://github.com/jasondavies/euclid-uniform-processes. https://palomar-registry.org/entry?id=PALOMAR-2026-10-23-000012&version=2.link
  2. J. Stein. Computational problems associated with Racah algebra. Journal of Computational Physics 1(3):397--405, 1967. doi:10.1016/0021-9991(67)90047-2 (https://doi.org/10.1016/0021-9991(67)90047-2).DOI
  3. Lou van den Dries and Yiannis N. Moschovakis. Is the Euclidean algorithm optimal among its peers? Bulletin of Symbolic Logic 10(3):390--418, 2004. doi:10.2178/bsl/1102022663 (https://doi.org/10.2178/bsl/1102022663).DOI
  4. Lou van den Dries and Yiannis N. Moschovakis. Arithmetic complexity. ACM Transactions on Computational Logic 10(1), Article 2, 49 pp., 2009. doi:10.1145/1459010.1459012 (https://doi.org/10.1145/1459010.1459012). Preprint: https://www.math.ucla.edu/~ynm/papers/ac.pdf.DOI

Version history

  1. v1Submitted by Jason DaviesInitial depositCurrentOct 28, 2026