Extended states in the Anderson model in dimension ν ≥ 3

Fix an integer $\nu\ge1$ and real numbers $a<b$ . Let $(V_\omega(x))_{x\in\mathbb Z^\nu}$ be independent random variables, each uniformly distributed on $[a,b]$ . The Anderson model is the random self-adjoint operator on $\ell^2(\mathbb Z^\nu)$ given by

(H_\omega u)(x)=\sum_{y\in\mathbb Z^\nu:\ |x-y|=1}u(y)\;+\;V_\omega(x)\,u(x).

The first term is the discrete Laplacian up to a constant shift, with spectrum $[-2\nu,2\nu]$ . The width $b-a$ measures the strength of the disorder. Almost surely $\sigma(H_\omega)=[-2\nu+a,\,2\nu+b]$ . By ergodicity, the absolutely continuous, singular continuous and pure point parts of the spectrum are also almost surely equal to fixed sets $\Sigma_{\mathrm{ac}},\Sigma_{\mathrm{sc}},\Sigma_{\mathrm{pp}}$ [2, 10].

Problem (Simon's Problem 1). Prove that for every $\nu\ge3$ there are $a<b$ , with $b-a$ small, and an open interval $I\subset\mathbb R$ such that, almost surely, $H_\omega$ has purely absolutely continuous spectrum in $I$ :

I\cap\sigma(H_\omega)\neq\emptyset,\qquad I\cap\Sigma_{\mathrm{pp}}=I\cap\Sigma_{\mathrm{sc}}=\emptyset .

Equivalently, the spectral projection $E_I(H_\omega)$ is nonzero, and for every $u\in\ell^2(\mathbb Z^\nu)$ the spectral measure of $u$ restricted to $I$ is absolutely continuous with respect to Lebesgue measure [2].

The expected answer is that for small disorder the spectrum near the band center is purely absolutely continuous, while it is pure point near the band edges, with a mobility edge between. Even the existence of a nonzero absolutely continuous component, for any $\nu\ge2$ and any $a<b$ , is unproved on $\mathbb Z^\nu$ . [1, 2, 15]

Background

Anderson introduced the model in 1958 to explain the absence of electrical conduction in disordered materials [1]. Physicists predict two regimes. In the localized regime, eigenfunctions decay exponentially and wave packets stay in a bounded region. In the extended regime, wave packets spread diffusively. Scaling theory predicts that in dimensions $1$ and $2$ every amount of disorder localizes all states. In dimension $\nu\ge3$ it predicts a localization–delocalization transition. Absolutely continuous spectrum is the spectral counterpart of extended states [14].

Simon listed this as the first of fifteen open problems in his 2000 list on Schrödinger operators [2]. The mathematical theory of localization is now well developed. Delocalization on $\mathbb Z^\nu$ has resisted all methods, because it requires control of the resolvent uniformly in time at energies inside the spectrum. Aizenman and Warzel give a modern account [10].

Known results

Localization. In dimension $1$ the spectrum is pure point for every $a<b$ [3]. In every dimension, localization holds at large disorder and near the band edges. The two main methods are multiscale analysis [4] and the fractional moment method [5].
Tree graphs. On the Bethe lattice (the regular tree), Klein proved purely absolutely continuous spectrum at weak disorder in compact subsets of the interior of the free spectrum [6, 7]. Froese, Hasler and Spitzer gave a geometric proof [8]. Aizenman, Sims and Warzel proved stability of the absolutely continuous spectrum [9]. Aizenman and Warzel found absolutely continuous spectrum well beyond the free spectrum [11].
Dynamics at weak coupling. For $\nu\ge3$ and potential $\lambda V$ , Erdős, Salmhofer and Yau proved that the evolution is diffusive up to times of order $\lambda^{-2-\kappa}$ for some $\kappa>0$ [12]. This does not reach the infinite-time statement needed for absolutely continuous spectrum.
Toy models. Disertori, Spencer and Zirnbauer proved diffusive behavior at low temperature for a supersymmetric hyperbolic sigma model in three dimensions, which is expected to reflect the extended phase [13].

References

Simon's Problems (2000) (proposed by Barry Simon)

P. W. Anderson, "Absence of diffusion in certain random lattices", Phys. Rev. 109 (1958), 1492–1505. doi:10.1103/PhysRev.109.1492
B. Simon, "Schrödinger operators in the twenty-first century", in Mathematical Physics 2000, Imperial College Press (2000), 283–288. doi:10.1142/9781848160224_0014
H. Kunz and B. Souillard, "Sur le spectre des opérateurs aux différences finies aléatoires", Comm. Math. Phys. 78 (1980), 201–246. doi:10.1007/BF01942371
J. Fröhlich and T. Spencer, "Absence of diffusion in the Anderson tight binding model for large disorder or low energy", Comm. Math. Phys. 88 (1983), 151–184. doi:10.1007/BF01209475
M. Aizenman and S. Molchanov, "Localization at large disorder and at extreme energies: an elementary derivation", Comm. Math. Phys. 157 (1993), 245–278. doi:10.1007/BF02099760
A. Klein, "Absolutely continuous spectrum in the Anderson model on the Bethe lattice", Math. Res. Lett. 1 (1994), 399–407. doi:10.4310/MRL.1994.v1.n4.a1
A. Klein, "Extended states in the Anderson model on the Bethe lattice", Adv. Math. 133 (1998), 163–184. doi:10.1006/aima.1997.1688
R. Froese, D. Hasler and W. Spitzer, "Absolutely continuous spectrum for the Anderson model on a tree: a geometric proof of Klein's theorem", Comm. Math. Phys. 269 (2007), 239–257. doi:10.1007/s00220-006-0120-3
M. Aizenman, R. Sims and S. Warzel, "Stability of the absolutely continuous spectrum of random Schrödinger operators on tree graphs", Probab. Theory Related Fields 136 (2006), 363–394. doi:10.1007/s00440-005-0486-8
M. Aizenman and S. Warzel, Random Operators: Disorder Effects on Quantum Spectra and Dynamics, Grad. Stud. Math. 168, AMS (2015). doi:10.1090/gsm/168
M. Aizenman and S. Warzel, "Resonant delocalization for random Schrödinger operators on tree graphs", J. Eur. Math. Soc. 15 (2013), 1167–1222. doi:10.4171/JEMS/389
L. Erdős, M. Salmhofer and H.-T. Yau, "Quantum diffusion for the Anderson model in the scaling limit", Ann. Henri Poincaré 8 (2007), 621–685. doi:10.1007/s00023-006-0318-0
M. Disertori, T. Spencer and M. R. Zirnbauer, "Quasi-diffusion in a 3D supersymmetric hyperbolic sigma model", Comm. Math. Phys. 300 (2010), 435–486. doi:10.1007/s00220-010-1117-5
Wikipedia, Anderson localization.
Wikipedia, Simon problems.

physics

AMR Open Problem Lists

Posted 2 months ago · edited 1 day ago

Progress summary

Refreshed 6 days ago

Open

The lattice problem remains open publicly, despite an unverified 2026 claim that OpenAI proved the expected weak-disorder result.

The problem asks for purely absolutely continuous spectrum for the standard Anderson operator on the lattice in dimensions three or more, at suitable weak disorder and in some energy range. It is identified with Simon’s 2000 problem; the 2009 workshop report records the lattice question as unresolved.

Known results

Klein (1994): on the Bethe lattice, sufficiently weak disorder gives purely absolutely continuous spectrum on closed intervals inside the free spectral interior.
Froese, Hasler, and Spitzer (2008): analogous weak-disorder results hold on specified tree-like graphs, subject to moment assumptions and finitely many exceptional energies.
Surveys and workshop reports through 2009 describe the corresponding lattice result in dimensions $d \ge 3$ as unproved.

Community submission (unverified), October 14, 2026

A submitted proof argues that an OpenAI preprint dated September 23, 2026 proves a nonzero purely absolutely continuous spectral restriction on an open interval for iid uniform disorder on $\mathbb{Z}^d$ , $d \ge 3$ , at sufficiently small fixed disorder. It also reports a Lean formalization, but no independent mathematical assessment was retrieved.

Current status (as of October 2026): The lattice problem remains open in the public record; the September 23, 2026 OpenAI claim and its formalization are unverified.

Sources

Claimed by OpenAI. For each fixed d>=3 and each fixed sufficiently small positive disorder, the manuscript claims the nearest-neighbor Anderson operator on Z^d with iid uniform site potentials has a nonzero purely absolutely continuous spectral restriction to an open interval I_d. The interval is independent of disorder strength; the threshold and probability-one event may depend on the fixed parameters. Global pure-ac spectrum and a mobility edge are not claimed.See full solutionHide full solution

Scope relative to this problem: For nearest-neighbor iid uniform site disorder on Z^d,d>=3, the source claims a nonzero purely absolutely continuous spectral restriction on an open interval at each fixed sufficiently small positive disorder. The interval is disorder-independent, but thresholds and probability-one events may depend on fixed parameters. This addresses an ac energy-range assertion, not global pure-ac spectrum, a mobility edge or quantum diffusion.

GitHub repository: https://github.com/openai/math

Manuscript: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Absolutely-Continuous-Spectrum-for-Weak-Disorder-Anderson-Models-in-Dimensions-at-Least-Three-September-23-2026/paper.pdf

OpenAI-261-01-Absolutely-Continuous-Spectrum-for-Weak-Disorder-Anderson-Models-in-Dimensions-at-Least-Three.pdf852,757 bytesOpen

ProofLean category, not Solution: a complete Lean 4 formalization of this problem, proving OpenAI's solution (Absolutely Continuous Spectrum for Weak-Disorder Anderson Models in Dimensions at Least Three, Thm 1.1). Repository cadamcat/anderson-ac-lean4, fixed version v1.0.0 (38116e1a), public 2026-10-14 09:09 UTC. Standard axioms only; fresh build, leanchecker and Comparator pass. The mathematics is OpenAI's; this post is the formalization.See full solutionHide full solution

Problem. Extended states in the Anderson model in dimension at least three: Simon's Problem 1 (B. Simon, Schrödinger operators in the twenty-first century, 2000, Example 2.1 and Problem 1), MathDB #389103.

Category. Lean. I, Yao Xu (@cadamcat), am the author of the formalization. I am not an author of the mathematical solution, which is OpenAI's, and I claim only the Lean category.

Corresponding mathematical solution. OpenAI, Absolutely Continuous Spectrum for Weak-Disorder Anderson Models in Dimensions at Least Three, OpenAI Math Release preprint dated September 23, 2026, fixed at openai/math commit adc7f1241b42e322a6451854ab7e4b4c146bf78a. Theorem 1.1 (§1.1). It is an unrefereed preprint; I know of no review record. The formalization follows the paper section by section and proves its Theorem 1.1.

Repository and version.

[
  {
    "repository": "https://github.com/cadamcat/anderson-ac-lean4",
    "branch": "main",
    "commit": "38116e1a08b2b3427f24d6043fffd5560fba6905"
  }
]

38116e1a08b2b3427f24d6043fffd5560fba6905 is the annotated tag v1.0.0. The repository was published as that single commit.
v1.0.1 (37cacdb1098857d82fe71793fc0afbcf56d723f3) changes no statement or proof. It cleans up comments, makes the docstring of Statement precise and adds the check Verification/NonVacuity.lean. With comments removed, every Lean file other than the new check is token-identical to v1.0.0.
v1.0.2 (51e7e5f40bbbe47e6be3f05eb0baac3081b12969) adds the verification record docs/verification.md; no Lean file changes.

Target theorem and statement.

Theorem: AndersonAC.Blueprint.anderson_challenge : AndersonChallenge.Statement, in AndersonAC/Blueprint/Main.lean, lines 37–38.
Statement: AndersonAC/Challenge.lean, lines 16–46. It imports Mathlib only and defines IsAndersonOperator, IsSpectralMeasure and Statement.

def Statement : Prop :=
  ∀ d : ℕ, 3 ≤ d → ∃ δ : ℝ, 0 < δ ∧ ∀ a b : ℝ, a < b → b - a < δ →
    ∃ E₁ E₂ : ℝ, E₁ < E₂ ∧
      ∀ (Ω : Type) [MeasureSpace Ω] [IsProbabilityMeasure (volume : Measure Ω)]
        (V : (Fin d → ℤ) → Ω → ℝ),
        (∀ n, Measurable (V n)) → iIndepFun V volume →
        (∀ n, pdf.IsUniform (V n) (Set.Icc a b) volume volume) →
        ∀ᵐ ω, (∃ T, IsAndersonOperator (fun n => V n ω) T) ∧
          ∀ T, IsAndersonOperator (fun n => V n ω) T →
            (∀ E ∈ Set.Ioo E₁ E₂, (E : ℂ) ∈ spectrum ℂ T) ∧
            (∀ v μ, IsSpectralMeasure T v μ → μ.restrict (Set.Ioo E₁ E₂) ≪ volume) ∧
            (∃ v, (∃ μ, IsSpectralMeasure T v μ) ∧ ∀ μ, IsSpectralMeasure T v μ → μ (Set.Ioo E₁ E₂) ≠ 0)

Statement correspondence.

Model (Simon, Example 2.1). IsAndersonOperator V T says (T u)(n) = Σ_{i<d} (u(n + e_i) + u(n − e_i)) + V(n) u(n) on ℓ²(ℤ^d), the nearest-neighbour operator with positive hopping. The paper uses negative hopping. The unitary (−1)^{x₁+⋯+x_d} exchanges the two conventions, and the formalization proves the transport (package signTransport).
Disorder. The potentials are any measurable, mutually independent family, each uniform on [a, b], on any probability space. This includes the paper's product space [−1,1]^{ℤ^d} after the affine change V = (a+b)/2 + ((b−a)/2)·ω, so the width b − a corresponds to the paper's coupling λ = (b − a)/2.
Quantifiers. For every d ≥ 3 there is δ > 0 such that for every width b − a < δ there is a nonempty open interval (E₁, E₂). The interval may depend on a, b, which is Simon's wording ("some energy range" at "suitable values of b − a"). The proof gives more: the paper's fixed interval I_d translated by the centre (a+b)/2 (AndersonAC.Blueprint.SimonProblem).
Conclusion (almost surely).
- The operator exists.
- (E₁, E₂) lies in the spectrum.
- Every spectral measure, restricted to (E₁, E₂), is absolutely continuous with respect to Lebesgue measure.
- Some vector has nonzero spectral weight in (E₁, E₂).
These are the paper's I_d ⊂ σ(H), χ_{I_d}(H) ℓ² ⊂ H_ac(H) and χ_{I_d}(H) ≠ 0, that is, purely absolutely continuous spectrum on a nonempty open energy range.
Spectral measures. IsSpectralMeasure T v μ (a finite measure on ℝ whose moments are ⟪v, Tᵏ v⟫) determines the spectral measure of v uniquely for bounded self-adjoint T, since the moments grow at most geometrically.
Non-vacuity.
- The conclusion asserts the existence of the operator and of a vector with nonzero spectral weight, so the "every spectral measure" clauses are not vacuous.
- The hypotheses are satisfiable. A separate Lean check, run against the published build of v1.0.0, proves two things with the standard axioms only:
  - hypotheses_satisfiable: for every d and a < b there is a probability space with a measurable, independent family indexed by ℤ^d whose members are uniform on [a, b] (Mathlib's exists_iid);
  - conclusion_witnessed: for every d ≥ 3, anderson_challenge then yields a potential, an operator satisfying IsAndersonOperator, a vector and a spectral measure of it with nonzero mass on (E₁, E₂).
Paper form. The paper's Theorem 1.1 in the OAI library's vocabulary is AndersonAC.Blueprint.PaperTheorem, proved as paperTheorem_blueprint. The packages lawTransport, signTransport, spectralTransport and challengeBridge derive Statement from it.
Independent statement review. A separate reviewer compared the statement with Simon's Example 2.1 and Problem 1 (author-posted TeX, mp_arc 00-78), the MathDB page and the manuscript's Theorem 1.1. Verdict: faithful, with notes. The model, width scaling, hopping convention, almost-sure conclusion, interval-in-spectrum clause and nonzero spectral weight match after the affine and unitary transports. The notes:
- The exported type lets the interval depend on a, b. That matches Simon's wording; the manuscript's fixed interval and its threshold formula are carried by the internal PaperTheorem and SimonProblem.
- MathDB's model synopsis does not state the single-site law. The statement follows Simon's uniform law on [a, b].

Toolchain and dependencies.

Lean leanprover/lean4:v4.34.1 (lean-toolchain).
OpenAI's library openai/math (subdirectory lean) at adc7f1241b42e322a6451854ab7e4b4c146bf78a, required in lakefile.lean.
Mathlib d13f23b723b8a846827a245b89c10fc7d3f11612.
All revisions are fixed in lake-manifest.json.

Reproduction.

git clone https://github.com/cadamcat/anderson-ac-lean4 && cd anderson-ac-lean4
git checkout 38116e1a08b2b3427f24d6043fffd5560fba6905
lake exe cache get
./scripts/verify.sh

verify.sh builds the library and prints the axioms of the final theorem and of the 17 package theorems (Verification/Axioms.lean). It fails on sorryAx or any axiom outside propext, Classical.choice and Quot.sound.

Axiom audit.

'AndersonAC.Blueprint.anderson_challenge' depends on axioms: [propext, Classical.choice, Quot.sound]

Every package theorem gives the same list. With comments removed, no Lean source in the repository contains sorry, admit, native_decide or an axiom declaration.

Independent verification of the fixed commit. These checks ran on a fresh clone of v1.0.0, with tool versions pinned:

clean build: exit 0, 9780 jobs, 1200 s with 10 threads;
leanchecker --fresh AndersonAC.Blueprint.Main: exit 0 (900 s);
Comparator ca04cfc7 with nanoda 3a240721, on a challenge module made from Challenge.lean with the theorem as sorry and no definition holes, so the three definitions must match exactly: exit 0, accepted by nanoda and by the Lean kernel;
the controls: nanoda accepts a correct proof and rejects a sorry proof and a tampered literal; Comparator rejects a challenge with 2 ≤ d in place of 3 ≤ d ("Const does not match … AndersonChallenge.Statement").

Original public date.

GitHub created_at: 2026-10-14T09:09:51Z.
The activity feed records the creation of refs/heads/main at 38116e1a08b2b3427f24d6043fffd5560fba6905 at 2026-10-14T09:10:00Z.
Software Heritage: save request 2556541, full visit at 2026-10-14T09:10:15Z, snapshot swh:1:snp:54653186a021ec4547ea70c275cf678e74636910, containing main at that commit and tag v1.0.0.
Git commit and tag dates are author-set metadata.

Public date and earlier work.

The formalization became public on 2026-10-14. The solution it formalizes became public in October 2026.
On 2026-10-14 I searched GitHub repositories for "anderson absolutely continuous lean" and "anderson model lean4". I found no other Lean formalization of this problem.

Attribution. Mathematical solution: OpenAI. Formalization: Yao Xu (AUTHORS.md). The proof builds on OpenAI's Lean library and on ported LeanPool and Tau Ceti code, all credited in THIRD_PARTY.md. The Lean formalization was prepared by the author with AI assistance; all proofs are verified by the Lean 4 kernel.