Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. For every there is a linear ordering of with no monotone -term arithmetic progression, so the answer is no for every .
[ABJ11] calls a linear ordering of a set chaotic when no distinct with satisfy , and proves (Theorem 4.1) that has a chaotic linear ordering. The ordering is built in three steps: the doubling recursion , gives a chaotic ordering of (Theorem 2.2); König's lemma transfers it to (Theorem 3.1); and with a basis of over , two reals are compared by the rational ordering at the first basis coordinate where they differ, and a progression holds coordinatewise, so a monotone progression in would give one in . A monotone -term progression contains a monotone three-term one, so the ordering has none of any length . The proof uses the axiom of choice through the existence of a basis; the paper asks whether a choice-free construction exists. Remark 1 of the paper adds, without written proof, that for each some ordering of has monotone -term but no -term progressions. The library card records the paper.
Acceptance. Refereed: Ardal, H., Brown, T. and Jungić, V., Chaotic
orderings of the rationals and reals, Amer. Math. Monthly 118 (2011), no. 10,
921–925 (the December 2011 issue, the date of this page). Reviewed: the site's
curator, Thomas Bloom, labels the problem disproved, states the negative answer
for every and credits it to [ABJ11]. The site's label DISPROVED (LEAN)
and the catalog statement Erdos194.erdos_194, marked solved with a
formal_proof link, point at a Lean file written with Aristotle and posted by
a forum user in the site's discussion thread on 2026-04-15, a formalization of
this result linked above; it follows the paper's construction and states its
own erdos_194, the existence of a linear ordering of with no
strictly increasing or decreasing -term progression for every , in
its own vocabulary rather than the catalog's. The file was not built or audited
by this corpus, so formalized is not listed.
Depends on. No wiki page; the claim rests on the cited paper.