Skip to content
#

random-schrodinger-operators

Star

Here is 1 public repository matching this topic...

cadamcat / anderson-ac-lean4

Star 0

Lean 4 proof of absolutely continuous spectrum for the Anderson model in dimension d ≥ 3 (Simon's Problem 1): for small uniform disorder the spectrum is almost surely purely absolutely continuous on an open energy interval; formalization with Mathlib

theorem-proving lean formal-verification mathematical-physics mathlib anderson-model lean4 formal-proof spectral-theory random-schrodinger-operators absolutely-continuous-spectrum
  • Updated Oct 15, 2026
  • Lean

Add this topic to your repo

To associate your repository with the random-schrodinger-operators topic, visit your repo's landing page and select "manage topics."

Learn more