Quotients of balanced ternary numbers
Guy's question F31: infinitely many integers are not a ratio of two numbers whose balanced-ternary digits are all 1 or −1.
Open problem settled, formally verified in Lean 4
Infinitely many integers that are not quotients of zero-free balanced ternary numbers
Let B be the positive integers whose balanced ternary digits are all 1 or -1. Selfridge and Lacampagne asked whether every integer not divisible by 3 is a quotient of two elements of B (Guy, Unsolved Problems in Number Theory, F31). Coppersmith found the exception 247, and Bai, Meleshko, Riasat and Shallit (Integers 22, 2022) found seventeen below 3650 and wrote that there are likely infinitely many, “but we have no proof”.
This paper proves it. 4·3^k + 5, 4·3^k − 5, 8·3^k + 7 and 8·3^k + 17 lie outside B/B for every k ≥ 5, and 8·3^k − 7 for every k ≥ 7, each bound sharp (Theorem 1.1); eight further families are exceptions along residue classes of k (Theorem 1.3). The proof finds, for each family, a set of carries of size linear in k that is closed under the carry map of multiplication by n and contains no accepting carry; for 4·3^k + 5 it is short enough to check by hand (Section 3). Of the 200 exceptions below 10^8, 75 are covered. One new data point for the companion problem with digits 0 and 1: 621·3^16 − 20 is an exception.
Preprint v1, 8 October 2026, not peer reviewed. Theorems 1.1 and 1.3 are formally verified in Lean 4 (lean/, standard axioms only), and every number quoted in the paper is recomputed by verify/check_paper.py; the exposition has not yet been independently reviewed. The author used an AI tool (Claude, Anthropic) in this work, as described in the paper’s declaration of generative AI use, and is responsible for its content.