Pure-point spectrum of the two-dimensional Anderson model
From OpenAI Aftermath
Pure-point spectrum of the two-dimensional Anderson model concerns the nearest-neighbour Anderson operator on the square lattice, the discrete Laplacian plus independent random site energies, and the conjecture that at every positive disorder its spectrum consists entirely of eigenvalues with a complete eigenbasis. A manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims this pure-point conclusion throughout the spectrum for independent uniform site potentials at every fixed positive disorder. The collection includes a Lean formalization of a supporting statement, the identification of the spectrum. This page summarizes the published claim 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.
Background
- As recounted in the introduction of the manuscript:
- Anderson introduced random site energies as a mechanism suppressing quantum transport, and the scaling theory of Abrahams, Anderson, Licciardello and Ramakrishnan predicts the absence of metallic behaviour in two dimensions. Simon's Problem 2 asks for the pure-point spectral type throughout the spectrum at every nonzero width of the uniform distribution.
- Fröhlich and Spencer's multiscale analysis, Fröhlich, Martinelli, Scoppola and Spencer, and Delyon, Lévy and Souillard proved localization at large disorder or extreme energies, and the fractional-moment method of Aizenman and Molchanov covers similar regimes. Ding and Smart proved localization near an edge for the two-dimensional Bernoulli model, extended by Hurtado; the final spectral step of the manuscript follows the rank-one mechanism of Simon and Wolff.
The original result
- Claim. Theorem 1.1 of Pure-Point Spectrum for the Two-Dimensional Anderson Model at Every Positive Disorder states that for each fixed h > 0 and independent site potentials uniform on [−h, h], the operator almost surely has pure-point spectral type, admits a complete orthonormal eigenbasis and has spectrum [−4−h, 4+h], with eigenvalues dense in this interval. The manuscript states that it does not assert one probability-one event for all disorder strengths, a bound uniform in energy, exponential eigenfunction decay or dynamical localization.
- Method, as described: at a fixed energy, absorbing terms on finite tori define scattering amplitudes and a Dirichlet energy on port data, which feed fractional Green-function moments under the uniform product law; a rank-one averaging argument in the style of Simon and Wolff turns the resulting square-summable resolvent columns into the spectral conclusion.
- Sources. The manuscript Pure-Point Spectrum for the Two-Dimensional Anderson Model at Every Positive Disorder at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization constructs the operator almost surely for every h > 0 and identifies its spectrum as [−4−h, 4+h], and that this selected statement does not assert the pure-point spectral type claimed in the manuscript. The Comparator statement is
PlanarAndersonSpectrum.lean. - The companion result in higher dimensions is described on Absolutely continuous spectrum of the Anderson model in dimension at least three.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 19–20 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math at commit adc7f12, tables at repository commit bb5fdb6, 18 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-10 | cert-machine, openai/math lane K, run 38019899278 (PlanarAndersonSpectrum) |
Verification (kernel replay) | Records that Lean's default kernel and the nanoda kernel both accept the solution of the challenge. | Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list PlanarAndersonSpectrum, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-12 | P. Lopatto, Mobility Edge for Sparse Complex Gaussian Matrices (Hexagon 2610.00168v1) | Remark (citation) | In its discussion of recent advances, the paper cites both manuscripts. It describes them as preprints produced by an internal OpenAI large language model that announce two results: purely absolutely continuous spectrum on a nonempty energy interval at weak disorder on Zd for d ≥ 3, and pure-point spectrum throughout the spectrum at every positive disorder on Z2. The paper's own results concern a mobility edge for sparse Hermitian random matrices on Erdős–Rényi graphs. | Hexagon (version 1). |
| 2026-10-13 | MColbrook/AIM, problem 016 (GitHub; AI for Mathematical Problems, checked 13 October 2026) | Catalogue | Lists Localization at every disorder strength in two dimensions as partially solved: the OpenAI manuscript gives pure-point spectral type and a complete orthonormal eigenbasis at every fixed positive disorder, while the problem as stated there asks for an eigenbasis of exponentially decaying eigenfunctions, which the manuscript does not assert. | Open-problem collection entry; status unchanged at repository commit 24edaad (15 October 2026).
|
| 2026-10-14 | chenle02/anderson-finite-core-lean (GitHub) | Formalization (Lean, partial) | A Lean 4 formalization of the finite-dimensional algebraic core of the two-dimensional manuscript, as a Comparator challenge and solution: the absorption and symmetric-unitarity identities of the scattering matrix, the closure formula, the single-port energy identity and an endpoint identity. The README states that the analytic, probabilistic and multiscale parts, which carry the localization claim, are not formalized and that nothing in the repository verifies the paper's theorem. | Repository; the README reports only the standard axioms. A later commit (af71973, 17 October 2026) records a Comparator receipt reporting a pass for the repository's own challenge.
|
| 2026-10-15 | chokmah-me/fragile-proof-audit, planar-anderson-spectrum (GitHub) | Review (statement correspondence) | A statement-level audit of the challenge PlanarAndersonSpectrum: it states the spectral set, the spectral-type content of the two-dimensional theorem is absent from the challenge (as the scope note says), and the dimension-at-least-three manuscript is not listed in the scope note. It also observes that the repository's formalization.yaml catalogue has no entry for this challenge. |
Read-only audit note; no build or Comparator run reported. |
| 2026-10-16 | J. Jardine, Lattice24, referee review rank_097 in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap, with one minor coverage note: three cell-level inputs to the comparison theorem (the transmission, relative cutoff and interior envelope estimates) were not checked line by line. | Part of an audit of the collection's manuscripts that the audit describes as complete. The review is published under CC BY 4.0. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The kernel and statement checks in the table concern the Lean statement of the spectrum, not the pure-point spectral type.
- Until 20 October 2026 these follow-ups were listed on Localization and delocalization in the Anderson model, which now gives an overview of both results.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
