Localization and delocalization in the Anderson model

2 papersLean

Resolves the predicted spectral contrast for the lattice Anderson model with independent uniform site potentials. In dimension two, every positive disorder strength gives almost surely pure-point spectrum. In every fixed dimension d ≥ 3, sufficiently weak positive disorder gives purely absolutely continuous spectrum on a fixed open interval with nonzero spectral weight.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

Absolutely Continuous Spectrum for Weak-Disorder Anderson Models in Dimensions at Least Three

OpenAI · September 23, 2026

For each fixed dimension d ≥ 3 and each fixed sufficiently small positive disorder strength, we prove that the Anderson operator on ℤ^d with independent uniform site potentials almost surely has purely absolutely continuous spectrum with nonzero weight on an open energy interval. The interval may depend on d but is independent of the disorder strength. This settles the purely absolutely continuous energy-range question in Simon's Problem 1 for this model.

Read PDF Download Source

Cite

@misc{OAI:Absolutely-Continuous-Spectrum-for-Weak-Disorder-Anderson-Models-in-Dimensions-at-Least-Three-September-23-2026,
  author = {{OpenAI}},
  title = {{Absolutely Continuous Spectrum for Weak-Disorder Anderson Models in Dimensions at Least Three}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Absolutely-Continuous-Spectrum-for-Weak-Disorder-Anderson-Models-in-Dimensions-at-Least-Three-September-23-2026/paper.pdf}{OAI:Absolutely-Continuous-Spectrum-for-Weak-Disorder-Anderson-Models-in-Dimensions-at-Least-Three-September-23-2026}},
  year = {2026}
}

Pure-Point Spectrum for the Two-Dimensional Anderson Model at Every Positive Disorder

OpenAI · September 23, 2026

For each fixed positive disorder strength, we prove that the nearest-neighbor Anderson operator on the square lattice with independent uniform site potentials almost surely has pure-point spectral type throughout its spectrum. This resolves the pure-point assertion of the two-dimensional Anderson localization conjecture for the uniform single-site law.

Read PDF Download Source

Cite

@misc{OAI:Pure-Point-Spectrum-for-the-Two-Dimensional-Anderson-Model-at-Every-Positive-Disorder-September-23-2026,
  author = {{OpenAI}},
  title = {{Pure-Point Spectrum for the Two-Dimensional Anderson Model at Every Positive Disorder}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Pure-Point-Spectrum-for-the-Two-Dimensional-Anderson-Model-at-Every-Positive-Disorder-September-23-2026/paper.pdf}{OAI:Pure-Point-Spectrum-for-the-Two-Dimensional-Anderson-Model-at-Every-Positive-Disorder-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Pure-Point Spectrum for the Two-Dimensional Anderson Model at Every Positive Disorder

Scope

The linked formalization proves a supporting spectral statement for the nearest-neighbor Anderson operator on \(\mathbb Z^2\). For every disorder strength \(h>0\) with independent site potentials uniform on \([-h,h]\), it constructs the bounded self-adjoint operator almost surely and identifies its spectrum as the real interval \([-4-h,4+h]\).

This selected statement identifies the spectral set. It does not assert the pure-point spectral type claimed in the accompanying paper.

Comparator links

Result	Comparator statement
Almost-sure spectrum of the planar Anderson operator	PlanarAndersonSpectrum.lean

Scope note on GitHub →