Localization and delocalization in the Anderson model
Localization and delocalization in the Anderson model is the subject of two manuscripts dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math). The Anderson model is the discrete Laplacian on the integer lattice plus a random potential with independent site values; Simon's Problem 1 asks whether, in dimension at least three and at weak disorder, it has absolutely continuous spectrum in some energy range. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original results
- Dimension at least three. For each fixed dimension d ≥ 3 and each sufficiently small positive disorder strength, the manuscript proves that the Anderson operator on Zd with independent uniform site potentials almost surely has purely absolutely continuous spectrum with nonzero weight on an open energy interval, which may depend on d but not on the disorder strength. It states that this settles the purely absolutely continuous energy-range question in Simon's Problem 1 for this model. Source: the manuscript Absolutely Continuous Spectrum for Weak-Disorder Anderson Models in Dimensions at Least Three, dated 23 September 2026.
- Dimension two. For each fixed positive disorder strength, the nearest-neighbour Anderson operator on the square lattice with independent uniform site potentials almost surely has pure-point spectrum throughout its spectrum; the manuscript states that this resolves the pure-point assertion of the two-dimensional localization conjecture for the uniform single-site law. Source: the manuscript Pure-Point Spectrum for the Two-Dimensional Anderson Model at Every Positive Disorder, dated 23 September 2026.
- Formalization, as described by the repository. The scope note lean/docs/261.md states that the formalization proves a supporting statement for the two-dimensional operator, identifying its spectrum as the interval [−4−h, 4+h], and does not assert the pure-point spectral type.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 14 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math at commit adc7f12, tables at repository commit cd0063d, 13 October 2026) |
Review (fidelity of the formal statements) | Rates this family "weaker-statement": the Lean identifies only the spectrum of the two-dimensional operator, while the headline claims about spectral type are not stated. Its per-challenge table records a sandboxed Comparator pass for the challenge PlanarAndersonSpectrum (8 October 2026). |
The review states that its ratings concern whether the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet. |
| 2026-10-08 | V. Jakšić, Y. Last, Extended States on the Bethe Lattice Revisited (arXiv:2610.11611, v1) | Remark | A short proof that the Anderson model on the Bethe lattice has purely absolutely continuous spectrum at weak disorder on compact intervals inside the free spectrum. The abstract observes that the same structural argument shortens the final passage from boundary positivity to purity in the OpenAI manuscript on Zd, d ≥ 3. | arXiv v1. |
| 2026-10-14 | Yao Xu, cadamcat/anderson-ac-lean4 (GitHub; commit 38116e1) |
Formalization (Lean) | A Lean 4 formalization of the dimension-at-least-three result, stated with Mathlib definitions only: for every d ≥ 3 there is a width bound such that, for independent site potentials uniform on any interval shorter than that bound, almost surely an open energy interval lies in the spectrum, every spectral measure is absolutely continuous on it, and some vector has nonzero spectral weight in it. The README states that the final theorem uses only the standard axioms and that the work was developed with AI assistance. | Author-reported. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.