An important question studied in Ergodic theory is the time average behavior of transformation on a measure space. A generalization of this considers multiple pairwise commuting transformations of a space, for which pointwise convergence is still an open conjecture, but for the weaker notion of norm convergence this is known. Variation estimates of norms give a notion that is weaker than pointwise convergence, but stronger than convergence in norm, and it is an ongoing project to prove variation estimates for commuting transformations. In this talk, I will describe progress towards formalizing these variation estimates for commuting transformations. This will require tools from analysis such as multilinear interpolation theory, the Calderón transference principle, and some refactors of Mathlib.