---

Claim. For integers $k_1,k_2\ge2$ let $f(k_1,k_2)$ be the least clique number of a graph in which every partition of the edges into two classes yields $k_1$ mutually adjacent vertices joined within the first class or $k_2$ within the second. Folkman's Theorem 1 (printed p. 20) proves

$$f(k_1,k_2)=\max(k_1,k_2).$$

With $k_1=k_2=3$ there is a graph of clique number $3$, hence with no $K_4$, every $2$-coloring of whose edges has a monochromatic triangle, which is what Problem 582 asks for; the answer is yes. The editor's note on p. 19 states this specialization, and the paper records that the question was first raised by Erdős for this case. The library's source card records the paper. The quantitative question, the least order $F_e(3,3;4)$ of such a graph, is not this problem's question; the problem page records the interval $21\le F_e(3,3;4)\le786$ from later sources as context.

Depends on. Nothing in this wiki; the result rests on the cited paper alone.

Acceptance. Refereed: J. Folkman, Graphs with monochromatic complete subgraphs in every edge coloring, SIAM J. Appl. Math. 18 (1970), no. 1, 19--24, received 30 November 1967 and printed in the January 1970 issue (by its Crossref record), the month this page is dated by; the day is a placeholder. The paper is posthumous and was published as first submitted, with editorial footnotes. Reviewed: the site's curator, T. F. Bloom, records in the problem's commentary that Folkman proved existence, with poor quantitative bounds, and credits the later bounds on the least order to Frankl and Rödl, Spencer, Lu, Dudek and Rödl, Bikov and Nenov, and Lange, Radziszowski and Xu (its key [Fo70]; page last edited 8 February 2026).

The Lean formalization. The site's label is PROVED (LEAN). The formal-conjectures statement of the problem names, in a formal_proof attribute, the file src/v4.29.1/ErdosProblems/Erdos582.lean of the repository lean-proofs of Boris Alexeev at the commit the link above pins, and a comment of 6 February 2026 in the site's thread announced that proof as a formalization of Folkman's result by Aristotle, an AI prover. The file declares itself a formalization of a solution to the problem, with Folkman as informal author and Aristotle and Boris Alexeev as formal authors, and proves erdos_582: a finite simple graph with clique number $3$ every two-coloring of whose edges has a monochromatic triangle, built on Folkman's construction; it has no sorry and records #print axioms as propext, Classical.choice and Quot.sound. It is a formalization of this claim, not an independent result, so it is a link here. Nothing was built, audited or kernel-checked in this corpus, so no formalized evidence is listed.

Read depth. The statement of Theorem 1 and the editor's specialization (printed pp. 19--20) were read; the proof, through the paper's Theorem 2 on vertex colorings, was not reconstructed. Nothing is independently reviewed in this corpus.