Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 183

claims/: The 1 claim page of Problem 183, one per claimant's result; the problem's standing derives from them.

Statement. Let $R(3;k)$ be the minimal $n$ such that if the edges of $K_n$ are coloured with $k$ colours then there must exist a monochromatic triangle. Determine

\lim_{k\to \infty}R(3;k)^{1/k}.

Status. Solved: the limit is $+\infty$ . The site labels the problem SOLVED (LEAN), with commentary crediting the proof to an internal model at OpenAI in the form $R(3;k)\ge k^{(1/3-o(1))k}$ for all $k\ge2$ (page last edited 1 September 2026), and hosts Rob Morris's seven-page exposition of the construction under its proof expositions. The source is OpenAI's August 6, 2026 version of Chapter 9, Theorem 1.1. The accompanying upstream Lean file is linked at a pinned revision; it was not built or independently audited in this repository. The claim page OpenAI 2026 records the theorem and its postings as an accepted claim: the acceptance evidence is the credit of the site's curator, T. F. Bloom, and Morris's signed exposition; the report is not refereed, and this project's review of its own reconstruction (under Current assessment) is not counted as acceptance. The frontmatter standing derives from that page.

Source. erdosproblems.com/183, accessed 2026-09-04 and 2026-10-07: the problem page, its discussion thread (six comments, none an objection) and its empty proof-claim tab. Cite as: T. F. Bloom, Erdős Problem #183, https://www.erdosproblems.com/183.

References.

[Wa97] Wan, Honghui, Upper bounds for Ramsey numbers $R(3,3,\cdots,3)$ and Schur numbers. J. Graph Theory 26 (1997), no. 3, 119--122, DOI 10.1002/(SICI)1097-0118(199711)26:3<119::AID-JGT1>3.0.CO;2-U (received 9 November 1990, revised 15 June 1993, per p. 119). Theorem 2.4, p. 121: $R(3;k)\le k!(e-e^{-1}+3)/2+1$ for $k\ge4$ , from Folkman's $R(3;4)\le65$ through a parity refinement of the Greenwood–Gleason recursion. A historical factorial upper bound, superseded by [XXC02] as given in Eliahou's Corollary 2 (see Known Results); it does not bear on the limit. Library home: wan_1997_upper_bounds_ramsey_numbers_r_3_3_3_schur_numbers and its theorem_2_4 page.
[Wh73] Whitehead, Jr., Earl Glen, The Ramsey number $N(3,\,3,\,3,\,3;\,2)$ . Discrete Math. 4 (1973), no. 4, 389--396, DOI 10.1016/0012-365X(73)90174-X (Crossref record accessed). The site's text prints no volume.
[XXC02] Xu, Xiao Dong and Xie, Zheng and Chen, Zhi, Upper bounds for Ramsey numbers $R_n(3)$ and Schur numbers (in Chinese). Math. Econ. 19 (2002), no. 1, 81--84 (volume and issue from the bibliography of Radziszowski's Small Ramsey numbers, Electron. J. Combin. DS1.18, revision of 24 April 2026; no Crossref record). The site's text prints no volume.
[Er61] Erdős, P., Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. 6 (1961), 221--254. A site key. Its item 20 of Part I (printed pp. 232--233) states Schur's theorem and the conjecture that the Schur numbers $f(n)$ satisfy $f(n)<c^n$ and $f(n)^{1/n}\to C$ , the question in its Schur-number form (read literally, Erdős's $f(n)$ is $S(n)+2\le R(3;n)$ , where $S(n)$ , the largest $N$ for which $\{1,\ldots,N\}$ has an $n$ -coloring with no monochromatic solution of $x+y=z$ , is at most $R(3;n)-2$ ); the paper states neither $R(3;k)$ nor a prize. The site's commentary records that Erdős offered a prize for showing the limit finite, the opposite of the answer. Library home: erdos_1961_unsolved_problems.
[El20] Eliahou, S., An adaptive upper bound on the Ramsey numbers $R(3,\ldots,3)$ . Integers 20 (2020), Paper A54, 7 pp. A site key, cited for more on the upper bound: its introduction surveys the upper bounds on $R(3;k)$ , and its Corollary 2 (p. 4) is the proof of the $k!(e-1/6)+1$ bound of [XXC02] from $R(3;4)\le62$ . Library home: eliahou_2020_adaptive_upper_bound_ramsey_numbers_r_3_3 and its corollary_2 page.
[He77] Heinrich, K., Proper colourings of $K_{15}$ . J. Austral. Math. Soc. 24 (Series A) (1977), 465--495, DOI 10.1017/S1446788700020838. Not a site reference; the classification of the good $3$ -colorings of $K_{15}$ that the computational proof of the finite bound $R_4(3)\le62$ consumes (see Known Results). Theorem 2, printed p. 485; the proofs read for structure only. Library home: heinrich_1977_proper_colourings_k_15 and its theorem_2 page.
[KaSt68] Kalbfleisch, J. G. and Stanton, R. G., On the maximal triangle-free edge-chromatic graphs in three colors. J. Combinatorial Theory 5 (1968), 9--20, DOI 10.1016/S0021-9800(68)80024-9. Not a site reference; the classification of the good $3$ -colorings of $K_{16}$ , the two seeds of every stage of the computational proof of $R_4(3)\le62$ and the classification [He77] assumes (see Known Results). The Theorem, printed p. 19, with the incidence matrices of Tables 2(a) and 2(b), p. 16; the proofs read for structure only. Library home: kalbfleisch_stanton_1968_maximal_triangle_free_edge_chromatic_graphs_three_colors (filed from the publisher's open archive) and its theorem_p19 page.
[LaMa88] Laywine, C. and Mayberry, J. P., A simple construction giving the two non-isomorphic triangle-free 3-colored $K_{16}$ 's. J. Combin. Theory Ser. B 45 (1988), 120--124, DOI 10.1016/0095-8956(88)90062-7. Not a site reference; the construction of both good $3$ -colorings of $K_{16}$ from four tricolored tetrahedra that the computational proof of $R_4(3)\le62$ cites in place of an edge table for its two seeds (see Known Results). The Lemma, printed p. 122, and the Theorem with the identification of the two classes, printed p. 123; the two proofs, a paragraph each, read in full. Library home: laywine_mayberry_1988_simple_construction_two_non_isomorphic_triangle_free_3_colored_k_16 (filed from the publisher's open archive) and its theorem_p123 page.

Formalization. The upstream statements are linked at a pinned revision; no build, axiom check or independent statement-fidelity review was performed in this repository. The formal-conjectures file ErdosProblems/183.lean, first added on 7 August 2026, states erdos_183 and erdos_183.variants.explicit_lower_bound under category research solved, with proof sorry and formal_proof attributes pointing at the ten-proofs file described below. See “Formalization and assessment limits” below for the exact source and scope.

Current assessment

The complete Chapter 9 lower-bound route is reconstructed in the library.

All five reconstructed proofs have passed a fresh independent whole-proof review and distinct report grading, including their composition and the full root-limit consequence. The lower-route review identifies the report version, exact native subjects, mathematical checks, and acceptance limits. They include every essential deduction in this lower-bound route. The earlier hat-guessing ingredients are reproved directly, so no unproved external theorem is required. Historical lower-bound sources remain outside this accepted lower-route scope; their earlier compilation obligations are unchanged. The separate elementary implication giving the refined factorial upper bound has independently reviewed premise-relative proof coverage, recorded in the upper-route review. Its finite computational premise remains claims-checked only. Within that finite route, the analytic attaching-set reduction has a complete reconstruction and independently reviewed proof coverage, including its degree lemma and elementary Ramsey bounds. The later structural and computational exclusions are separate obligations; this reduction changes no catalog status or formal standing.

Search scope: the report (its relevant chapter in full), its first-party announcement, the pinned formalization sources and the identified matrix/cover predecessor. The catalog page's last edit is dated 1 September 2026, so the formulation above, taken on 2026-09-04, is unchanged. This bounded search does not assert a comprehensive literature search or an independent community-acceptance review.

The lower-route review examined this page as it stood on 2026-09-09, and the upper-route review and grade as it stood on 2026-09-10. Since then the References, the Status field and the Known Results sentences that cite [He77], [KaSt68], [LaMa88] and [Wa97] at statement depth were added or rewritten; the statement, the lower-bound route and its reviewed proofs were not changed.

Progress

OpenAI's technical report gives an absolute constant $c>0$ such that, for every integer $k\geq2$ ,

R(3;k)\geq\left(\frac{ck^{1/3}}{\log k}\right)^k.

The logarithm is natural, and coloring by $k$ colors does not require using every color. Since $k^{1/3}/\log k$ tends to infinity, this bound determines the requested limit. No upper bound or general limit-existence theorem is needed for this deduction.

The report was announced by OpenAI on August 1, 2026. Its author is OpenAI; the announcement attributes the arguments to an internal model and manuscript preparation to humans working with that model. This is a source-supported solution, distinct from a claim of journal refereeing. The review of the library's reconstruction of the lower-bound route is recorded separately above.

Known Results

Lemma 2.1 constructs a saturated matrix, and Lemma 2.2 turns it into a fixed two-sided coordinate cover. Lemma 2.3 supplies many separated palettes of omitted colors. Proposition 3.1 uses those ingredients to color recursively while excluding monochromatic triangles and retaining proper vertex labels in every color graph. Theorem 1.1 combines the palette counts, controls the ceiling jumps and extends the bound to every $k\geq2$ .

For quantitative context, a separate compilation-supplied upper route derives $R(3;k)\leq(e-1/6)k!+1$ for every integer $k\geq4$ from Fettes–Kramer–Radziszowski, Theorem 5.6, the published finite bound $R(3;4)\leq62$ . The finite theorem was checked at statement depth only; its computational proof is not locally reviewed. One classification that proof consumes, that every good $3$ -coloring of $K_{15}$ is one of the two obtained from the good $3$ -colorings of $K_{16}$ , is [He77]'s, recorded at statement depth on Heinrich, Theorem 2; the classification of $K_{16}$ it rests on, that there are exactly two good $3$ -colorings of $K_{16}$ up to renaming vertices and permuting colors, the two seeds of every stage of that proof, is [KaSt68]'s, recorded at statement depth on Kalbfleisch and Stanton, Theorem, which also transcribes the two seeds' incidence matrices from its Tables 2(a) and 2(b). The construction of both seeds that the same proof cites in place of an edge table, four tricolored tetrahedra properly joined into a super-TCT, the untwisted seed with an even and the twisted seed with an odd number of positive joinings, is [LaMa88]'s, recorded at statement depth on Laywine and Mayberry, Theorem; the completeness of the seed list remains [KaSt68]'s. This elementary upper implication has independently reviewed premise-relative proof coverage only. It does not change the accepted lower route, the solved status or any verification tier, and does not revalidate current-record wording.

Formalization and assessment limits

The upstream MulticolorTriangleRamsey.lean at the linked commit contains erdos_183 for the divergent root limit and erdos_problem_183_explicit for that limit together with the all- $k\geq2$ lower bound using $c=1/(6e^{38})$ . This repository examined only its Ramsey definitions and endpoint statements. The full proof and dependency closure were not audited, and no Lean build, axiom check or independent statement-fidelity review was performed in this repository. The source digest records the exact toolchain, dependency pin and upstream verification reports.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

Linked from (38)

problems/ramsey_theory/E0183/claims Problem 554 Ramsey Theory number_theory/erdos_1961_unsolved_problems Ramsey Theory ramsey_theory/ageron_2021_new_lower_bounds_schur_weak_schur Corollary 2.9: the growth rate of the Schur numbers and of R_n(3) is at least 380^{1/5} ≈ 3.28 Inequality (6): S(n + 5) ≥ 380 S(n) + 148 Theorem 2.3: an S-template of width q and a sum-free k-partition of [1, p] give a sum-free partition of [1, pq + m_{n+1} − 1]ramsey_theory/eliahou_2020_adaptive_upper_bound_ramsey_numbers_r_3_3 Corollary 2: R_n(3) ≤ n!(e − 1/6) + 1 for all n ≥ 4 ramsey_theory/exoo_1994_lower_bound_schur_numbers_multicolor_ramsey Lower bound, p. 2: a sum-free partition of [1, 160] into five sets, so S(5) ≥ 160 and R_5(3) ≥ 162 An Upper Bound of 62 on the Classical Ramsey Number R(3,3,3,3)Section 5 - The reported computation behind Theorem 5.6 Theorem 3.2 - A bounded attaching set in a good four-colouring of K62 Theorem 5.6 - No good four-colouring of K62 ramsey_theory/fredricksen_2000_symmetric_sum_free_partitions_lower_bounds Constructions, pp. 6–8: symmetric sum-free partitions of [1, 536] into six sets and of [1, 1680] into seven, so S(6) ≥ 536 and S(7) ≥ 1680 ramsey_theory/heinrich_1977_proper_colourings_k_15 Theorem 1 (p. 479): every proper 3-coloring of K_15 has 35 edges in each color Theorem 2: exactly two proper 3-colorings of K_15, each embedded in a proper 3-coloring of K_16 ramsey_theory/heule_2017_schur_number_five Main result: S(5) = 160, the fifth Schur number, by a machine-checked unsatisfiability proof ramsey_theory/kalbfleisch_stanton_1968_maximal_triangle_free_edge_chromatic_graphs_three_colors Theorem (p. 19): exactly two non-isomorphic triangle-free 3-colorings of K_16 ramsey_theory/laywine_mayberry_1988_simple_construction_two_non_isomorphic_triangle_free_3_colored_k_16 Theorem (p. 123): the super-TCT colorings of K_16 form exactly two isomorphism classes Ten Advances in Mathematics and Theoretical Computer Science Chapter 9 - Super-exponential lower bounds for multicolour triangles Chapter 9, equation (2) - Refined factorial upper bound Chapter 9, Lemma 2.1 - Saturated matrices Chapter 9, Lemma 2.2 - Two-sided coordinate cover Chapter 9, Lemma 2.3 - Separated palettes Chapter 9, Proposition 3.1 - Recursive triangle-free colourings Chapter 9, Theorem 1.1 - Superexponential triangle Ramsey growth ramsey_theory/wan_1997_upper_bounds_ramsey_numbers_r_3_3_3_schur_numbers Theorem 2.4: r_n ≤ n!(e − e⁻¹ + 3)/2 + 1 for n ≥ 4, the n-color Ramsey number of the triangle

Graph