Claims

../

1941_01_01_turan: Turán (Mat. Fiz. Lapok 1941): in its triangle case, a graph on n vertices with more than floor(n^2/4) edges contains a triangle; with the complete bipartite graph this gives f_2(n) = floor(n^2/4) + 1; refereed.

1962_03_01_erdos: Lemma 1 of Erdős's 1962 paper, found jointly with Gallai and independently by Andrásfai, with its sharpness example: f_3(n) = floor((n-1)^2/4) + 2 for every n at least 5; refereed, in Illinois J. Math.

2024_04_11_ren_wang_wang_yang: A preprint of April 2024 (v2 October 2025) proving that f_4(n) = floor((n-3)^2/4) + 6 for every n at least 90, attained by blow-ups of the Grötzsch graph; a preprint with no journal record, so claimed.

2026_09_10_kentakitamura: A forum comment of 10 September 2026 announcing a Lean 4 development said to determine f_4(n) for every n, extending the preprint's range; read as text only, unreviewed and not accepted by the site.

2026_09_19_kentakitamura: A forum comment of 19 September 2026 announcing a kernel-checked Lean 4 proof that f_5(n) = floor(n^2/4) - 3n + 15 for every n >= 80; read as text only, unreviewed and not accepted by the site.

---