SemicircleLaw

This contains information about the formalization of Wigner's Semicircle Law in Lean. The project began as a Stanford Undergraduate Research Institute in Mathematics (SURIM) summer research project. The proof we will follow is contained in the first 18 pages of Todd Kemp's RMT notes. We will then try to remove the moment assumptions on the entries and formalize up through page 23.

Links to the github repository and project website are below.

• github.com/FredRaj3/SemicircleLaw (Repository)

• fredraj3.github.io/SemicircleLaw/ (Project Site)

Week 1 Intro Worksheet: pdf, LaTeX

Week 1 Intro Presentation: slides

Week 2 Intro Computations and Linear Algebra: pdf

Mathlib naming conventions

Other interesting reading: 

1. Foundations 

2. Mathematics and the Formal Turn 

3. LeanSearch paper 

4. Lean pitfalls 

5. LeanHammer paper