A directed cut in a directed graph is the set of directed edges from one part 
to the other part 
of a set partition of the
vertex set into two parts. Write 
for the number of these directed
edges. In contrast to an undirected cut, 
and 
can differ (Folz and Tyomkyn 2026).
Folz and Tyomkyn (2026) proved that, for every fixed integer 
and sufficiently large 
, every loopless directed graph
with 
directed
edges, no repeated ordered edges, and minimum outdegree at least 
has a set partition of its
vertex set into two parts satisfying
![min{e(A,B),e(B,A)}>=[((d-1)m+d^2)/(2(2d-1))],](/images/equations/DirectedCut/NumberedEquation1.svg) |
where ![[x]](/images/equations/DirectedCut/Inline10.svg)
is the ceiling function. Oppositely directed
edges are allowed. The bound is sharp for infinitely
many 
.
For 
, the weaker bound ![[m/6]](/images/equations/DirectedCut/Inline13.svg)
holds for every 
. Folz and Tyomkyn (2026) report that LLMs obtained the proofs with human input, that the authors revised them, and
that they were verified in Lean.
