---

Claim. Every $2$-coloring of the positive integers has a monochromatic three-term arithmetic progression $x,x+d,x+2d$ with $d>x$, the question of Problem 645, by the following argument, which the site's curator records in the problem's commentary and attributes to Ryan Alweiss. Suppose a red/blue coloring has no such progression and, by symmetry, that $1$ is red. Then $3$ and $5$ are not both red, since $1,3,5$ has $d=2>1$. If $3$ is blue and $n\ge6$ is red, the triple $1,n,2n-1$ forces $2n-1$ blue and the triple $3,n+1,2n-1$ then forces $n+1$ red; so the coloring is constant from some point on, and a monochromatic progression with $d>x$ follows. If $5$ is blue, the triples $1,n,2n-1$ and $5,n+2,2n-1$ show that a red $n$ forces $n+2$ red once $n$ is large enough, so the coloring is eventually constant on a residue class modulo $2$, and again such a progression follows. The site states the threshold of the second case as $n\ge8$; the triple $5,n+2,2n-1$ has difference $n-3$, which exceeds $5$ only from $n=9$ on, so the step needs $n\ge9$ (at $n=8$ the triple $5,10,15$ has $d=x$ and gives nothing). With that index the argument is correct, as the problem page's authored check records. The result is the same as Brown and Landman's Theorem 7 at $f(a)=a+1$, which has its own claim page; this page records the second, independent argument.

Depends on. Nothing in this wiki; the argument is the site's own case analysis.

Acceptance. Formalized. This corpus's verification built Boris Alexeev's repository plby/lean-proofs at the commit of 2026-09-15 that the formalization link pins, in its src/latest folder (Lean v4.33.0, Mathlib v4.33.0): the solution module ErdosProblems.Erdos645 and the comparator challenge Erdos645. It checked the axioms of Erdos645.erdos_645, which are exactly propext, Classical.choice and Quot.sound. The comparator challenge ComparatorChallenges/ErdosProblems/Erdos645.lean states that declaration with a sorry body, and the fingerprint of the solution's declaration was found identical to the challenge's. The statement was audited clause by clause against the problem's Statement: every coloring c : ℕ → Bool has $x\ge1$ and $d>x$ with $c(x)=c(x+d)=c(x+2d)$. Since $x>0$, the color of $0$ is never used, so this is the site's question for 2-colorings of the positive integers, as the Formulation reads $\mathbb N$, and exactly this page's claim; $d>x\ge1$ rules out degenerate progressions, and only natural-number addition and multiplication occur. It matches the Formal Conjectures statement erdos_645 verbatim. The built proof follows this page's argument: the case of $3$ blue, the case of $5$ blue with $n=8$ settled by a separate finite check, and complementation for the case of $1$ blue. What was built is the src/latest copy, whose header names Tom C. Brown, Bruce M. Landman, Ryan Alweiss and ChatGPT 5.1 Pro as its informal authors and Aristotle and Boris Alexeev as its formal authors. The src/v4.24.0 copy, which the Formal Conjectures file names as its formal proof, states the same theorem, but one of its tactic steps is the search exact?, and it was not built. The original file was produced by the automated pipeline that the thread's comment of 23 November 2025 reports: ChatGPT wrote the argument out (the comment's note names the model as gpt-5-nano; the file's header names ChatGPT 5.1 Pro) and Aristotle from Harmonic turned it into Lean. The built src/latest copy is a later revision of that file in the same repository, copied from it in May 2026 and revised since; the build certifies that revision, not the pipeline's original output. Not reviewed: the site's curator, T. F. Bloom, publishes the argument in the problem's commentary as a proof that the answer is yes, credits Alweiss by name, and labels the problem PROVED (LEAN) (page last edited 4 April 2026); but that commentary, written by the curator directly, is the argument's only posting (Alweiss posted nothing on the site, and its proof-claim tab is empty), so the curator published the claim rather than reviewing a claim published by another, and the curator's credit is not an independent review. Not refereed: no paper states the argument. The index defect is in the commentary's text, not in the mathematics, and does not affect the standing.

Postings and dating. The site's commentary carries no date. The site's history view, as of 2026-10-07, shows the argument already present in its earliest listed revision, of 20 October 2025, and that date names this page; the thread's comment of 23 November 2025, which says ChatGPT wrote out this argument for the formalization, is the first dated reference to it, and the community database records the problem proved since that day. Both thread comments declare AI assistance: the reference search used GPT5, and the original formalization came from the pipeline of ChatGPT and Aristotle described under Acceptance, of which the built copy is a later revision.