---

The claim. Let $A$ be the set of integers whose base-$3$ digits are all $0$ or $1$ and $B$ the set of integers whose base-$4$ digits are all $0$ or $1$. The file APNOutputs/ErdosProblems/erdos_125.variants.positive_lower_density.lean of DeepMind's public repository google-deepmind/alphaproof-nexus-results proves, as target_theorem_0, the formal-conjectures statement answer(False) ↔ 0 < (A + B).lowerDensity: the lower density of $A+B$ is not positive, which answers the question of Problem 125 in the negative. The statement is the one proved by DeepMind's accepted result of March 2026; the two are recorded apart because this file names no informal author, its proof runs through different lemmas, and no source says that it is that result's artifact.

Argument, in outline. The lemma names and statements indicate the following. A gap lemma (A_B_gap) shows that no integer strictly between $(3^k-1)/2+(4^m-1)/3$ and $\min(3^k,4^m)$ lies in $A+B$, since the elements of $A$ below $3^k$ are at most $(3^k-1)/2$ and those of $B$ below $4^m$ at most $(4^m-1)/3$. The irrationality of $\log 4/\log 3$ (log_ratio_irrational) gives, by a Dirichlet-type approximation (dirichlet_approx), exponents with $3^k\leq 4^m\leq(1+\epsilon)3^k$, so that the gap is a fixed fraction of the scale. A scale step (scale_step) then shows that a bound $\lvert(A+B)\cap[0,N)\rvert\leq CN$ at one scale yields the bound $\tfrac{11}{12}CN'$ at a larger scale $N'$, and induction (density_multi_scale) gives, for every $d$, some $N$ with $\lvert(A+B)\cap[0,N)\rvert\leq(11/12)^dN$; hence (density_tends_to_zero) the count falls below $\epsilon N$ for some $N$ at every $\epsilon>0$, which is the negation of positive lower density. The proof has not been reconstructed in this corpus.

Provenance. The claimant is DeepMind, whose repository holds the file under a Google LLC copyright header. The repository describes itself as the Lean proofs generated by AlphaProof Nexus for the paper of that name, with the ErdosProblems/ folder serving its section on autonomously solving open Erdős problems; it was created on 2026-05-13, and the one commit touching the file, "Results for AlphaProof Nexus", was authored on 2026-05-13 and committed on 2026-05-19, which dates this page. The commit was made from the GitHub account aferr; it publishes the system's output and claims no authorship, so the page lists no author, and the result is credited to the system, AlphaProof Nexus (Google DeepMind). The file carries EVOLVE-BLOCK markers around its lemmas and its proof, names no person, and names its system only through the repository and the commit message: AlphaProof Nexus. It imports the formal-conjectures utilities and contains no sorry. It runs to 22,480 bytes and 370 lines and was neither built nor audited in this corpus, so no kernel credit is claimed and formalized is not listed as evidence. Whether AlphaProof Nexus is the "DeepMind prover agent" that the site's thread names for the March result is not stated by the sources.

Acceptance. None listed. The site's curator credits the lower-density result to DeepMind through the thread's posting of March 2026, recorded on that result's page, and no comment or commentary on the site, and no other known record, refers to this file.

Depends on. No page of this wiki.