Analysis of a left-shift binary GCD algorithm (Shallit–Sorenson 1994), with a proof of its sum-of-squares conjecture
A complete Lean 4 formalization of Jeffrey Shallit and Jonathan Sorenson, "Analysis of a Left-Shift Binary GCD Algorithm" (J. Symbolic Computation 17, 1994). LSBGCD replaces (u, v) by v and the distance from u to the nearer of the shifted multiples 2^e v and 2^(e+1) v, where 2^e v ≤ u < 2^(e+1) v. The formalization proves that the algorithm computes the gcd, and proves Theorem 1.1: for every n, the lexicographically least ordered input taking exactly n iterations, its six closed forms in powers of 2 ± √3, and the order-16 linear recurrence satisfied by both coordinates. It proves in full…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-22-000018
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000018/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000018/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'