Double groupoids and cross modules are higher-dimensional categorical structures relevant to algebraic topology, but their formalization in a proof assistant had not been carried out, leaving the equivalence between these two frameworks unverified by machine.

The paper formalizes double groupoids and cross modules in the Lean theorem prover. Double groupoids generalize groupoids to higher dimensions, while cross modules capture 2-dimensional algebraic information. The formalization encodes the categorical structure and establishes the equivalence between the two frameworks within Lean.

The formalization demonstrates Lean's capability for encoding higher categorical structures and provides a machine-checked proof of the equivalence between double groupoids and cross modules.