The site labels the problem PROVED (LEAN); the suffix refers to a third-party Lean proof of the problem's statement, the case $k_1=k_2=3$ of Folkman's theorem, described under Formalization, which this corpus has not built. Folkman's 1970 theorem supplies the required graph, and this classical existence theorem is sufficient; the quantitative problem of finding the least possible order remains open. The claim page Folkman 1970 records the refereed theorem, its specialization to the question, the site's acceptance and the Lean proof as a formalization link. The later refereed upper bounds on the least order each prove the existence the problem asks for and have their own claim pages: Frankl and Rödl 1986, Spencer 1988, Lu 2008, Dudek and Rödl 2008 and Lange, Radziszowski and Xu; the lower bounds of Radziszowski and Xu and of Bikov and Nenov settle nothing about existence and have none. The frontmatter standing derives from them. The site lists a prize without saying which offer it records; the offers the sources describe all concern the least order $F_e(3,3;4)$, not existence: Erdős's 1975 offer for deciding whether fewer than $10^{10}$ vertices suffice, which Spencer [Sp88] met; Erdős's later offer for fewer than $10^6$ vertices, which Lu claims with $9697$; and Graham's 2012 offer for a proof that $F_e(3,3;4)\le100$ (Lange, Radziszowski and Xu, Table 1), which is open.