Computations about formal multiple zeta spaces defined by binary extended double shuffle relations

The formal multiple zeta space we consider with a computer is an $\mathbb{F}_2$-vector space generated by $2^{k-2}$ formal symbols for a given weight $k$, where the symbols satisfy binary extended double shuffle relations. Up to weight $k=22$, we compute the dimensions of the formal multiple zeta spaces, and verify the dimension conjecture on original extended double shuffle relations of real multiple zeta values. Our computations adopt Gaussian forward elimination and give information for spaces filtered by depth. We can observe that the dimensions of the depth-graded formal multiple zeta spaces have a Pascal triangle pattern expected by the Hoffman mult-indices.