Partial Hadamard Matrices in the Cubic Regime

Damek Davis

A Lean 4 formalization of the first-order asymptotic expansion for the number of partial Hadamard matrices when the number of columns grows cubically in the number of rows.