• All Packages
  • Criteria
    • All Packages
    • Criteria
  • Readme
  • Versions (1)
  • Dependencies (15)

FredRaj3SemicircleLaw

Formalization of Wigner's Semicircle Law in Lean
#math #probability #random-matrix-theory

METADATA

  • MIT
  • 17 hours ago
    Last updated on July 25, 2025 at 11:54:59PM
  • 2 stars

LEAN

  • Commit ac683bf fails to build on leanprover/lean4:v4.22.0-rc4
    v4.22.0-rc4
  • Commit 197df57 fails to build on leanprover/lean4:v4.22.0-rc3
    v4.22.0-rc3
  • Commit 6c99d80 builds on the recent leanprover/lean4:v4.22.0-rc2
    v4.22.0-rc2
  • Commit 1464c13 (latest) builds on its recent leanprover/lean4:v4.21.0
    v4.21.0
  • Commit f3972e7 builds on the recent leanprover/lean4:v4.21.0-rc3
    v4.21.0-rc3
  • Commit 9f0f43c builds on the recent leanprover/lean4:v4.20.1
    v4.20.1
  • Commit d1d2a02 builds on the recent leanprover/lean4:v4.20.0
    v4.20.0
  • Commit 9f0f43c builds on the old leanprover/lean4:v4.20.0-rc5
    v4.20.0-rc5
  • Commit d1d2a02 builds on the old leanprover/lean4:v4.19.0
    v4.19.0
  • 2 less

HOMEPAGE

fredraj3.github.io/SemicircleLaw/

REPOSITORY

FredRaj3/SemicircleLaw

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.

Get Started

  • Install
  • Learn
  • Community
  • Reservoir

Documentation

  • Language reference
  • Lean API
  • Use cases
  • Cite Lean

Resources

  • Lean playground
  • VS Code extension
  • Loogle
  • Mathlib

FRO

  • Mission
  • Team
  • Roadmap
  • Contact

Policies

  • Privacy Policy
  • Terms of Use
© 2025 Lean FRO. All rights reserved.