Addario-Berry et al. conjectured that every digraph on n vertices with more than (k-1)n arcs contains every antidirected tree with k arcs. This generalises the Erdős–Sós conjecture.

A diregularity-lemma approach reduces the problem to embedding the tree into the blow-up of an antidirected caterpillar inside the reduced digraph. The tree is decomposed into seeds and small pieces and assigned via homomorphisms to a caterpillar. Separately, an AI-generated proof of the Erdős–Sós conjecture is adapted to the antidirected setting using a permutation-marking counting argument. That adaptation has a Lean 4 formalisation by DeBiasio.

The paper proves dense approximate versions of the conjecture for bounded-degree antidirected trees and for trees with evenly distributed layers. It derives an asymptotic Burr's conjecture for bounded-degree antidirected trees and linear Ramsey bounds. It also gives a full proof of the conjecture by extending the AI proof, with a Lean 4 formalisation available.