Claims

../

1959_09_01_erdos_gallai: Theorem (2.6) of Erdős and Gallai (Acta Math. Acad. Sci. Hungar. 1959): a graph on n vertices with more than (k-1)n/2 edges contains a path with k edges, the statement of Problem 548 for every path on k+1 vertices.

2026_09_03_adamczewski: A Lean proof, found by GPT-6 Astra and published in Adamczewski's repository, that every graph on n vertices with at least (k-1)n/2 + 1 edges contains every tree on k+1 vertices; accepted on Lean built here.

2026_09_04_reed_stein: A 2026 preprint of Reed and Stein proving that for every positive gamma there is n_0 such that the statement of Problem 548 holds for all n at least n_0 and all k at least gamma n; a preprint, credited in the site's remarks.

2026_09_07_debiasio: Two papers by DeBiasio, written with GPT-6 Astra and formalized in Lean, prove Kalai's tight-tree conjecture for hypergraphs and the antidirected-tree conjecture for digraphs; each implies Problem 548; the Lean is not built here.

2026_09_14_riordan_scott: An arXiv note of Riordan and Scott simplifying GPT-6 Astra's argument: it proves the Erdős–Sós conjecture with its extremal graphs and the antidirected-tree conjecture for digraphs; a preprint.

2026_09_18_frederickson: An arXiv paper of Frederickson giving a simplified proof of the Erdős–Sós conjecture, based on GPT-6 Astra's resolution, and another proof of the antidirected-tree conjecture for digraphs; a preprint.

---