Status
On this page
Status
Topics
Status
On this page
Status
Topics
If is 2-coloured then must there exist a monochromatic three-term arithmetic progression such that ?
Source: erdosproblems.com/645
An accepted solution exists. The statement is true.
The site labels the problem PROVED (LEAN), a label it explains as a positive solution whose proof has been checked in Lean. The question is proved. The status-defining source is Theorem 7 of Brown and Landman (Bull. Austral. Math. Soc. 60 (1999), 21--35, refereed; paged here by the authors' own version): for every function from the positive integers to the positive reals, exists; the first proof shows directly that every 2-coloring of the positive integers has a monochromatic three-term progression with , and is this problem. The site's elementary argument, attributed to Ryan Alweiss, is checked below as an authored verification and is correct with one index adjusted, and a Lean proof of it was built and audited in this corpus (see "Formalization and the Lean label" below). The site's further remark that the statement fails for four-term progressions is true (Brown and Landman's Theorem 12 with , ), but the explicit coloring the site and Erdős offer as a witness does not have the property (an observation made here, below). The claim pages Brown and Landman 1999 and Alweiss's argument record the two proofs, their postings and their standing: Brown and Landman's theorem is accepted on its refereed publication and the curator's credit, and Alweiss's argument, whose only posting is the curator's own commentary, is accepted on the Lean proof built and audited here; the frontmatter standing derives from them.