---

Claim. The repository linked above holds two papers, each with a Lean development, that prove strengthenings of the statement of Problem 548.

• The hypergraph theorem, Kalai's conjecture: if an $r$-uniform hypergraph $H$ contains no copy of a given tight $r$-uniform tree with $m$ edges, then $r|E(H)|\le(m-1)|\partial H|$, where $\partial H$ is the shadow, the set of $(r-1)$-sets contained in an edge. At $r=2$ a tight tree is a tree and the shadow is a set of at most $n$ vertices, so a graph $G$ on $n$ vertices with no copy of a tree with $k$ edges has $2e(G)\le(k-1)n$.
• The digraph theorem, the conjecture of Addario-Berry, Havet, Linhares Sales, Reed and Thomassé: a loopless digraph $D$ with no copy of a given antidirected tree on $t$ vertices has $|A(D)|\le(t-2)|V(D)|$. Every tree has an antidirected orientation (all arcs from one side of its bipartition to the other), and the symmetric digraph of a graph $G$ has $2e(G)$ arcs, so with $t=k+1$ a graph with no copy of a tree on $k+1$ vertices has $2e(G)\le(k-1)n$.

Either bound is incompatible with $e(G)\ge\frac{k-1}2n+1$, so each theorem implies the statement for every $n\ge k+1$ and every tree on $k+1$ vertices.

Submission note. Posted to the site's forum by Louis DeBiasio on 7 September 2026:

I'm not sure if I should comment here or in the main problem section. In trying to understand the new proof, I used GPT-6 Astra to help improve the exposition of the original. Additionally, I had GPT-6 Astra both prove and formalize two strengthenings of the Erdős-Sós conjecture. One was a conjecture of Kalai on tight trees in hypergraphs. The other was a conjecture Addario-Berry, Havet, Linhares Sales, Reed, and Thomass'e on anti-directed trees in digraphs.

The proofs and lean formalizations are here https://github.com/louisdebiasio/erdos-sos

Claimant and postings. Louis DeBiasio, whose repository's README describes its contents as papers by DeBiasio using ChatGPT 6 Astra. DeBiasio's comment of 7 September 2026 on the site's proof claim for the problem says they had GPT-6 Astra both prove and formalize two strengthenings of the Erdős--Sós conjecture, and links the repository, first committed on the same day; the page is named by that date. The repository also holds an exposition of the claimant's proof of Adamczewski 2026, which is not part of this claim.

Standing. Claimed, not accepted. The README says both Lean projects use Lean 4.19.0 with no external package and that an axiom audit is part of their build; this corpus has not built or audited them, so they give no formalized evidence. No outside reviewer has examined the papers, and nothing is refereed. The antidirected-tree theorem is also proved in the papers of Riordan and Scott and Frederickson.

Depends on. Nothing in this wiki.

Read depth. The README, the repository's folder listing and the comment were read; the papers and the Lean sources were not.