---

Claim. Let $S$ be the smallest set of positive integers that contains $1$ and is closed under $x\mapsto2x+1$, $x\mapsto3x+1$ and $x\mapsto6x+1$, the set $A$ of Problem 1134. For every $\epsilon>0$ there is a constant $C(\epsilon)$ with

$$|S\cap[0,T]|\le C(\epsilon)\,T^{\tau_1+\epsilon} \quad\text{for all }T,$$

where $\tau_1\approx0.900526$ is the unique positive root of $6^{-\tau}+\sum_{k\ge0}(3\cdot2^k)^{-\tau}=1$. Since $\tau_1<1$, the set has natural density zero, so its lower density is zero and the problem's question is answered no. The result is Theorem 6 of J. C. Lagarias, Erdős, Klarner, and the $3x+1$ problem, Amer. Math. Monthly 123 (2016), no. 8, 753--776, which heads the theorem "(Crampin and Hilton)": the paper records that Erdős offered a prize for the question in 1972, that Crampin and Hilton answered it in the negative soon afterwards without publishing (the fact is reported in Klarner's 1982 paper, p. 140), and that the printed proof is the author's reconstruction. The proof rests on the relation $f_2\circ f_2\circ f_3=f_6\circ f_2$, which shows the semigroup is not free, so every generating word can be rewritten to avoid the pattern $62$; the rewritten words are words in an infinite set of free generators, and Theorem 3 applied to that free semigroup bounds their number, and so the count of $S$ below $T$, by $O(T^{\tau_1+\epsilon})$. The library pages are the source card and its result page Theorem 6; the earlier orbit bound, Theorem 3, gives nothing here because $1/2+1/3+1/6=1$.

Claimant and date. The page is filed under Lagarias, the author of the paper that first posts a proof; the theorem is attributed to Crampin and Hilton throughout. The page name's date is the Crossref record's creation date for the paper (28 September 2016; the issue is October 2016). The paper's section 7 is the only published proof found.

Acceptance. Refereed: the paper appeared in The American Mathematical Monthly, volume 123 (2016). Reviewed: the site's curator, Thomas Bloom, labels the problem DISPROVED (LEAN), last edited 9 January 2026, and the commentary attributes the negative answer to Crampin and Hilton with the bound above and names Lagarias's paper for the proof; on 2026-09-05 the proof-claim tab was empty. The site's commentary prints the exponent as $0.900626$; the paper prints $0.900526$ on p. 767, and the paper's figure is used here. The result page records how far the proof is compiled in the library, and this page rests on no review of its own.

Formalization. The file src/latest/ErdosProblems/Erdos1134.lean of the repository plby/lean-proofs, linked above, with its module Erdos1134/Dirichlet.lean holding the sublinear bound, declares itself a formalization of this result: its header names D. J. Crampin and A. J. W. Hilton as the informal authors and AxiomProver, published by Axiom Math, as the formal author, and its theorem not_erdos_1134 denies positive lower density. It is a copy of the development that the discussion thread's first post (19 June 2026) announced as AxiomProver's proof that the lower density is zero, the file Erdos/Erdos1134/solution.lean of the repository AxiomMath/erdos-public, which names no informal author and so presents itself as an independent proof, recorded on its own claim page. The copy is not built or audited here, so it is linked and not counted as formalized. The site's (LEAN) suffix is its catalog label. The formal-conjectures file ErdosProblems/1134.lean, added on 19 September 2026, states three things. It states the question as erdos_1134 under category research solved, with a formal_proof attribute pointing at the plby/lean-proofs copy. It states the sublinear bound as erdos_1134.variants.sublinear, also solved, with a formal_proof attribute pointing at the copy's Dirichlet.lean. It states the Klarner variant below as an open variant. It is a statement file with sorry bodies, not a proof, so it is linked here and not listed under links. The thread's second post (20 September 2026) claims a Lean proof that the Klarner variant with generators $2x$, $3x+2$, $6x+3$ has natural density zero, in the repository KitaKen1/erdos-1134-lean with a formal-conjectures pull request; it concerns the variant, not the site's statement, and is not linked.

Scope. Full for the site's statement. Klarner's variants with other generators are distinct questions, which the paper's section 9 reports unanswered as of 2016 and the problem page records: the site's variant is Klarner's question, the orbit of $0$ under $2x$, $3x+2$, $6x+3$, which Lagarias (pp. 771--772) and the site identify with Guy's Problem E36, although Guy's printed E36 starts the orbit from $1$; the thread's second post claims an answer for the orbit of $0$.