Gcd in O(log a / log log a) remainder calls refutes Moschovakis’s uniform-process conjecture
Awaiting review
The takeaway
Van den Dries and Moschovakis asked whether Euclid’s algorithm is optimal among algorithms that compute the gcd from the remainder function. On 29 Oct Jason Davies posted on Hexagon a proof that every pair a ≥ b has a derivation of gcd(a, b) using O(log a / log log a) remainder calls, while Euclid needs order log a in the worst case. That refutes Moschovakis’s conjectured logarithmic lower bounds for uniform processes and answers a closure-depth question of van den Dries and Moschovakis; Moschovakis’s Main Conjecture for actual algorithms stays open. GPT-6 Astra found the principal result in Codex; GPT-6 Astra and Claude Opus 5.5 wrote the Lean proofs and the paper, and Palomar’s comparator confirms the 22 compared statements. Davies says he wrote none of the text or code.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- 3 of 5
- Last verified
- 29 October 2026
Your AI and this story
- GPT-6 Astra182 days after its cutoff
- Claude Opus 5.5121 days after its cutoff
- Gemini 4 Argon212 days after its cutoff
- Grok 4.7151 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 121 days before it.
Key facts
- Claim (abstract, verbatim): ‘every pair a ≥ b has a derivation of gcd(a, b) from a, b with O(log a/ log log a) applications of the remainder function alone; Euclid’s algorithm needs order 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 ... The Main Conjecture for algorithms remains open.’
- Also: G(a, b) ≥ (1 − o(1)) log log N for all but o(N²) coprime pairs, and for each ε > 0 a nondeterministic register program with a successful computation using at most ε log a + O(1) remainder calls; the upper coefficient sharpens to 3 + o(1)
- AI transparency statement (verbatim): ‘The main result, its formalisation in Lean and the manuscript were produced by artificial intelligence. The human author initiated the broader research and directed the AI systems, but did not write the text.’
- Provenance (Hexagon, verbatim): ‘The principal result was identified by GPT-6-Astra (OpenAI), used through Codex ... 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.’ Palomar PALOMAR-
2026-10-23-000012(version 2); Moschovakis’s best-uniform-process theorem is cited, not formalised - Contributor: Jason Davies (jasondavies.com), who also posted the AI-generated ‘Hankel determinants and the length of finite Pierce expansions’ (Hexagon 2610.00588, 27 Oct)
- Verification status: Lean-verified main bounds (Palomar comparator); unrefereed preprint; Hexagon human understanding ‘some parts’; no expert reaction or HN thread found on 29 Oct
What happened
Euclid’s algorithm computes gcd(a, b) with about log a remainder operations in the worst case. Yiannis Moschovakis and Lou van den Dries asked whether any algorithm built from the same primitive can do essentially better, and Moschovakis conjectured logarithmic lower bounds, both for algorithms and for his more general “uniform processes”.
Davies’s paper shows that a derivation may store one short Euclidean prefix and reuse it many times, which brings the count down to O(log a / log log a). That kills the uniform-process versions of the conjecture. Whether a genuine algorithm (a finite program) can do the same is still open. GPT-6 Astra found the idea during a broader investigation Davies started; GPT-6 Astra and Claude Opus 5.5 then proved it in Lean and wrote the paper.
Why it matters
It is a small but clean answer to a question from the foundations of algorithms, and an example of a fully machine-written paper whose main claims a reader can check by running Lean rather than by trusting the text.
What is disputed or not yet verified
| Verification | Main bounds and refutations Lean-verified (Palomar comparator, 22 statements, two kernels); unrefereed Hexagon preprint |
|---|
Sources
3 sources from 2 sites. Numbers match the chips in the text.
3 sources: 3 primary
Primary
- Hexagon 2610.00604: The Euclidean algorithm is not optimal among uniform processes (Davies)hexagonmath.org, paper
- Palomar registry entry PALOMAR-2026-10-23-000012palomar-registry.org, code
- Hexagon 2610.00588: Hankel determinants and the length of finite Pierce expansions (Davies)hexagonmath.org, paper
Changes
- Filed (Hexagon API record and PDF of 2610.00604)