---

Claim. The file Erdos/Erdos1134/solution.lean of the repository AxiomMath/erdos-public, at the commit linked above, proves erdos_1134 : lowerDensity (setOf ErdosSetA) = 0: the smallest set of positive integers containing $1$ and closed under $x\mapsto2x+1$, $x\mapsto3x+1$ and $x\mapsto6x+1$, the set $A$ of Problem 1134, has lower density zero, so the problem's question is answered no. The file (714 lines, importing Mathlib) defines the set inductively from $1$ under the three maps, defines the lower density as the liminf of $|A\cap[0,N]|/N$, and reaches the theorem through a sublinear count with exponent $19/20$; its text contains no sorry, axiom declaration or native_decide and prints no axioms. The file carries no author header and names no informal author or source, so it presents itself as an independent proof. The thread's first post (19 June 2026) presents it as the work of AxiomProver, Axiom Math's prover, as the post names it. The corpus has not built, kernel-checked or audited the file.

Standing. Claimed: no outside acceptance of the file exists, since the site's label DISPROVED (LEAN) credits Crampin and Hilton's answer as published by Lagarias, recorded on Lagarias's claim page, and the corpus has not audited the formal statement. A copy of this development in the repository plby/lean-proofs, whose header names Crampin and Hilton as the informal authors, is linked from Lagarias's page as a formalization of that result; the formal-conjectures file for the problem points at that copy.

Depends on. No page of this wiki.