Circular law for sparse random matrices with independent row slices at sufficiently large logarithmic degree, with Lean 4/mathlib proofs, manuscript, and reproducible verification.
probability formal-verification mathlib random-matrices lean4 formalized-mathematics circular-law sparse-random-matrices row-regular
-
Updated
Oct 11, 2026 - Lean