---

Claim. There is a permutation of the positive integers with no subsequence of the form $a,a+r,a+2r,a+3r$ with $r$ a nonzero integer, so not every permutation of $\mathbb{N}$ contains a monotone four-term arithmetic progression and the answer to the question is no. Both index directions are covered, since $r$ may be negative.

The construction works on the nonnegative integers and shifts by one at the end. It orders them by the lowest binary digit at which two numbers differ, the number with digit $1$ there coming first. Three consecutive terms of an arithmetic progression alternate at that digit, so the middle term of a three-term progression never lies between its ends in this order, and four consecutive terms $a,b,c,d$ satisfy $a\lhd b$ exactly when $c\lhd d$. A finite word of distinct integers is safe when the order that puts the word first and the remaining integers in the binary order has no four-term progression. Every finite set listed in reverse binary order is safe, and an extension lemma shows that every safe word is a prefix of a safe word containing any prescribed finite set; applying it to the sets $\{0\},\{1\},\{2\},\ldots$ gives nested safe prefixes whose union is the permutation, by a computable procedure. The preprint records that GPT-6 Pro was used to find the construction and to produce its first draft. The author's repository formalizes the theorem in Lean 4 with Mathlib as FourAP.exists_fourAPFree_positive_permutation, a bijection of the positive integers avoiding every progression with nonzero integer difference, with the explicit computable permutation as witness; the file is linked above and was not built or audited by this corpus.

Postings. The preprint was submitted to arXiv on 2026-09-11 and the repository was created the same day, with its Lean statement and axiom audit; the arXiv link was added to it on 2026-09-14. The same question is answered no by the construction of Kruer and Kohlmeyer, certified by the bounty site Conjectures.io and recorded on its claim page: the bounty site verified that proof, before this preprint, while the first public postings of it found are of 14 September 2026, after it. The two constructions share their shape: both grow nested finite prefixes whose completion by the binary order, in which the middle term of a three-term progression never lies between its ends, is kept free of four-term progressions. The site's proof-claim thread for Problem 196 points to this preprint in a comment; the site's page does not list it as a proof claim.

Acceptance. None recorded: the preprint is not refereed, no outside reviewer has accepted it, the site's curator has not commented on it, and the Lean file is the author's own and was not built by this corpus, so the claim stays claimed. It answers the site's question as the accepted claim does, from which the problem's standing derives.

Depends on. No wiki page; the claim rests on the preprint and its Lean file.