SemicircleLaw

Formalization of Wigner’s Semicircle Law in Lean

Our goal is to formalize Wigner’s Semicircle Law in Lean. The result we will formalize is Theorem 2.3 in Todd Kemp’s Random Matrix Theory notes. The proof will be via the moment method.

Our project relies on the Lean blueprint tool by Patrick Massot.

The project webpage contains the blueprint and dependency graph.

This project is a Stanford Undergraduate Research Institute in Mathematics (SURIM) summer research project.