SURIM 2025

For our Stanford Undergraduate Research Institute in Mathematics (SURIM) summer research project, we'll be formalizing Wigner's Semicircle Law in Lean. The proof we will follow is contained in the first 18 pages of Todd Kemp's RMT notes. If time permits, we will 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