A cochain-level Adem relation? The original paper on Steenrod squares, Steenrod's "Products of cocycles and extensions of mappings", 1947, uses an explicit combinatorial formula for the squares in terms of simplicial cochains: given a simplicial cochain $\alpha$ on some simplicial set, Steenrod defines a cochain $\mathrm{Sq}^i\alpha$; if $\alpha$ is a cocycle, so is $\mathrm{Sq}^i\alpha$, and the cohomology class of $\mathrm{Sq}^i\alpha$ only depends on that of $\alpha$, and so $\mathrm{Sq}^i$ descends to a (linear!) map on cohomology. (In general, $\mathrm{Sq}^i$ is not linear on cochains and does not commute with $\mathrm d$, so this is a nontrivial statement. But it is not too hard to find an operation that agrees with $\mathrm{Sq}^i$ on cocycles and that does commute with $\mathrm d$, and its failure to be linear, it is not hard to show, is a total derivative.) (Steenrod makes his definition with $\mathbb Z$-coefficients, but I will only care about $\mathbb Z/2$ coefficients, and so assume that throughout.)
The well-known Adem relations, due originally to Adem,  "The iteration of the Steenrod squares in algebraic topology", 1952 and beautifully explained by Bullett and Macdonald, "On the Adem relations", 1982, are relations of the form $0 = \sum_{\text{certain pairs }(i,j)} \mathrm{Sq}^i \mathrm{Sq}^j$ that hold in cohomology. The first few are
 $\mathrm{Sq}^1 \mathrm{Sq}^1 = 0$, $\mathrm{Sq}^1\mathrm{Sq}^2 = \mathrm{Sq}^3 \mathrm{Sq}^0$, $\mathrm{Sq}^1 \mathrm{Sq}^3 = 0$, $\mathrm{Sq}^3 \mathrm{Sq}^1 = \mathrm{Sq}^2 \mathrm{Sq}^2$, ...
At the cochain level, these relations do not hold on the nose. The fact that they hold on cohomology just says that, if $\alpha$ is a cocycle, then $\sum_{\text{certain pairs }(i,j)} \mathrm{Sq}^i (\mathrm{Sq}^j(\alpha))$ is a coboundary, which of course depends on $\alpha$ (and on the particular relation in question).
Is there a combinatorial formula (like the one Steenrod gives for $\mathrm{Sq}^i$) that takes in $\alpha$ a cocycle and produces a primitive for $\sum_{\text{certain pairs }(i,j)} \mathrm{Sq}^i (\mathrm{Sq}^j(\alpha))$? Where can I find it? I care only about the early Adem relations up to $\mathrm{Sq}^3\mathrm{Sq}^1 = \mathrm{Sq}^2\mathrm{Sq}^2$.
A related question was asked by Kapustin. Note that I am not after more categorical descriptions of the Adem relations and the Steenrod squares like those available in the many excellent answers to this old MO question — I really do want a combinatorial description that fits into the framework of Steenrod's original paper.
 A: The following article might be relevant.  This is the review I wrote for it a number of years ago.
MR1622630 (99h:55027) Reviewed
Real, Pedro(E-SEVLIS-AM1)
On the computability of the Steenrod squares. (English, Italian summary)
Ann. Univ. Ferrara Sez. VII (N.S.) 42 (1996), 57–63 (1998).
55S05 (55S10)
Let $C_∗(X)$ denote the normalized chains on a simplicial set $X$. The Eilenberg-Zilber theorem can be proved using very explicit operators $AW:C_∗(X×Y) \rightarrow C_∗(X)\otimes C_∗(Y)$, $EM:C_∗(X)\otimes C_∗(Y) \rightarrow C_∗(X×Y)$, and $SHI:C_∗(X×Y)→C_{∗+1}(X×Y)$. The contracting homotopy SHI is least familiar, but like EM it involves an explicit summation over shuffles.
   The author gives an explicit and clean cochain level formula for the mod 2 Steenrod operation $Sq^i$ in terms of AW and SHI. Like SHI, it is exponential in terms of computational complexity.
   {Reviewer's remark: The author systematically uses the word "idempotent'' where he seems to mean "involution''.} 
A: Explicit homotopies for a cochain-level Adem relation were first worked out in:
Greg Brumfiel, Anibal M. Medina-Mardones, John Morgan. A Cochain Level Proof of Adem Relations in the Mod 2 Steenrod Algebra. 2020
The odd-prime case is still open.
