---

Claim. For the two-color van der Waerden number $W(k)$ of Problem 138, $W(k)/2^k\to\infty$, the question Erdős asked in [Er80] and the problem's commentary records, as the formal-conjectures variant erdos_138.variants.dvd_two_pow with the answer True. The result is a Lean 4 proof, the file Atlas/FC/Erdos138_dvd_two_pow_solution.lean of Meta's repository facebookresearch/atlas-lean (branch prepare-atlas-v2, added 2026-08-28), which carries Meta's copyright and names no author. The repository's README describes ATLAS, Autoformalized Textbook Library At Scale, as a Lean library of textbook mathematics formalized with large language models and generated with the AutoformBot pipeline; the system is named here as that README names it. The proof's lemmas combine Berlekamp's finite-field colorings over a set of distinct primes whose sum is about $k-1$, through sequences of traces of powers of primitive elements of the fields $\mathbb F_{2^p}$, into a two-coloring of an interval of length $M\prod_{p}(2^p-1)$ with no monochromatic $k$-term progression, which gives $W(k)>(n+1)2^k$ for every $n$ once $k$ is large. The argument was not reconstructed in this corpus.

Covers. The question $W(k)/2^k\to\infty$ of [Er80]. Not covered: the example question $W(k)^{1/k}\to\infty$, settled by the OpenAI release on its claim page, and the upper bound. The same question is answered by the explicit bound of Campos, Fox and Schildkraut, which the formal-conjectures file calls an independent proof (their claim page).

Depends on. No page of this wiki.

Standing. Claimed. The Atlas file is a Lean development with no informal write-up and no refereed publication, and it does not declare itself a formalization of any named claimant's result, so it has its own page. A verified copy, AtlasFCSolutions/Erdos138.lean of niketp03/atlas-fc-verified (2026-09-13), imports the formal-conjectures problem file, removes the Atlas file's local copies of the definitions monoAP_guarantee_set, monoAPNumber and W so that every definition in the statement is formal-conjectures' own, ends with the formal-conjectures theorem's name and statement with the answer filled in and a #print axioms line, and reports in its README a build with only propext, Classical.choice and Quot.sound. The formal-conjectures file for the problem, at its commit of 2026-10-06, marks the variant research solved with that copy as its formal_proof. The site labels the problem OPEN and its commentary does not mention the proof. This corpus has not built or audited either file, so the page lists no formalized evidence.