Proved. The site labels the problem proved and formalized, crediting GPT-6 Astra with the full proof, and the corpus accepts that result on the claim page (Adamczewski, 2026) on reviewed and formalized evidence: the pinned Lean development was built here, its axioms found to be the three standard ones, its compared declaration matched to the comparator challenge and its statement audited against the Statement above, and three arXiv papers by mathematicians independent of the claimant and the curator affirm the proof (Riordan and Scott, Wood, and Frederickson; Current assessment, below), so the problem stands solved and proved. The site's own acceptance is not an independent review, since its curator submitted the proof-claim entry and co-wrote the publication, and nothing is refereed. The sharp tree-free edge bound also establishes the classical strict threshold $e(G)>(k-1)n/2$. The formal verification and the preliminary state of the human-readable exposition are distinguished below. Three further proofs of stronger theorems are paged as claimed full claims: DeBiasio 2026 (two strengthenings proved with GPT-6 Astra, with Lean), Riordan--Scott 2026 and Frederickson 2026. Two partial claims are paged beside them: the Erdős--Gallai path case (accepted, refereed) and the Reed--Stein dense case (claimed, a preprint).