pith. sign in

arxiv: 2606.23821 · v1 · pith:3NGRQVYTnew · submitted 2026-06-22 · 🧮 math.NA · cs.AI· cs.HC· cs.NA· math.SP

Ten Digits on a Train: AI-Assisted Verification of Two Eigenvalue Problems

Matthew J. Colbrook This is my paper

Pith reviewed 2026-06-26 07:19 UTC · model grok-4.3

classification 🧮 math.NA cs.AIcs.HCcs.NAmath.SP
keywords eigenvalue certificationSchrödinger operatornon-normal operatorsKrawczyk-Brouwer inclusionDirichlet-Neumann bracketingresonance computationprojective matchingAI-assisted verification
0
0 comments X

The pith

AI-assisted methods certify the complete negative spectrum of a singular Schrödinger operator to ten decimals and separate a non-normal resonance pair to ten digits each.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how verified zero counts and Dirichlet-Neumann bracketing can certify every negative eigenvalue of a singular self-adjoint Schrödinger operator to ten decimal places. It also separates a previously unresolved resonance pair in a non-normal atom-molecule benchmark and encloses each member to ten digits by recasting the problem as a global matching system on projective solution lines. The infinite tail is treated as uncertainty in the terminal projective data, and a componentwise tail-robust Krawczyk-Brouwer inclusion supplies the rigorous certificate. The work illustrates that AI can rapidly generate candidate solutions and strategies, yet human verification remains essential because some AI-produced arguments omit required checks such as componentwise inclusion over nonuniform polydiscs.

Core claim

For the singular self-adjoint Schrödinger operator the complete negative spectrum is certified to ten decimal places by a verified zero count together with Dirichlet-Neumann bracketing. For the non-normal benchmark a previously unresolved resonance pair is separated and each resonance is enclosed to ten digits by reformulating the eigenvalue problem as a global matching system for projective solution lines, encoding the infinite tail as uncertainty in the terminal projective data, and applying a componentwise tail-robust Krawczyk-Brouwer inclusion.

What carries the argument

Global matching system for projective solution lines that encodes the infinite tail as uncertainty in terminal projective data, together with a componentwise tail-robust Krawczyk-Brouwer inclusion that supplies the certificate.

If this is right

  • The full negative spectrum of singular self-adjoint Schrödinger operators can be certified to high precision without relying on one-way shooting.
  • Non-normal eigenvalue problems with uncertain asymptotic data become rigorously solvable by projective matching rather than direct propagation.
  • Validated computation yields not only numerical values but proof objects that can expose gaps in AI-generated arguments.
  • The same architecture applies directly to other analytic boundary-value systems that suffer ill-conditioned propagation.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The method could be tested on higher-dimensional or time-dependent singular operators to check whether the projective matching still isolates resonances at ten-digit accuracy.
  • Software libraries for validated numerics may need built-in componentwise checks over polydiscs to prevent the specific omission that occurred in one AI tail argument.
  • Peer-review standards for computational mathematics papers may evolve to require deposit of the full proof objects rather than only the final digits.

Load-bearing premise

The reformulation as a global matching system correctly encodes the infinite tail as uncertainty in the terminal projective data and the componentwise Krawczyk-Brouwer inclusion supplies a valid certificate.

What would settle it

An explicit computation showing that the componentwise Krawczyk-Brouwer inclusion fails to hold in a nonuniform polydisc for the resonance problem, or that the verified zero count misses an eigenvalue of the Schrödinger operator.

Figures

Figures reproduced from arXiv: 2606.23821 by Matthew J. Colbrook.

Figure 1
Figure 1. Figure 1 [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 3
Figure 3. Figure 3 [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figure 3
Figure 3. Figure 3 [PITH_FULL_IMAGE:figures/full_fig_p010_3.png] view at source ↗
Figure 3
Figure 3. Figure 3 [PITH_FULL_IMAGE:figures/full_fig_p012_3.png] view at source ↗
Figure 1
Figure 1. Figure 1 [PITH_FULL_IMAGE:figures/full_fig_p013_1.png] view at source ↗
Figure 4
Figure 4. Figure 4 [PITH_FULL_IMAGE:figures/full_fig_p014_4.png] view at source ↗
Figure 4
Figure 4. Figure 4 [PITH_FULL_IMAGE:figures/full_fig_p015_4.png] view at source ↗
Figure 1
Figure 1. Figure 1 [PITH_FULL_IMAGE:figures/full_fig_p015_1.png] view at source ↗
Figure 1
Figure 1. Figure 1 [PITH_FULL_IMAGE:figures/full_fig_p023_1.png] view at source ↗
read the original abstract

Accurate numerical eigenvalues are often difficult to certify, especially in singular or non-normal settings. This article reports a human--AI collaboration on two such computations. For a singular self-adjoint Schr\"odinger operator, a verified zero count and Dirichlet--Neumann bracketing certify the complete negative spectrum to ten decimal places. For a delicate non-normal atom--molecule benchmark, a previously unresolved resonance pair is separated, with each member enclosed to ten digits. The second result is achieved not by increasing the precision of one-way shooting, but by reformulating the problem as a global matching system for projective solution lines. The infinite tail is encoded as uncertainty in the terminal projective data, and a componentwise, tail-robust Krawczyk--Brouwer inclusion supplies the certificate. This gives a reusable architecture for analytic boundary-value systems with ill-conditioned propagation and uncertain asymptotic data. The collaboration also exposes the strengths and limits of AI assistance. AI rapidly produced accurate candidates and plausible proof strategies, but several failed, including one apparently complete tail argument that omitted the componentwise check required by a nonuniform polydisc. Validated computation is a stringent test of AI-assisted mathematics: the output is not merely a number, but a number with a proof. These examples show why the proof object matters, and why human mathematical judgment remained decisive. More broadly, as AI makes code, exposition, and plausible numerical claims inexpensive, standards for verification, attribution, peer review, and training must adapt. The implications are unsettling; the opportunity is extraordinary.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper reports a human-AI collaboration verifying two eigenvalue problems to ten decimal places. For a singular self-adjoint Schrödinger operator, a verified zero count combined with Dirichlet-Neumann bracketing certifies the complete negative spectrum. For a non-normal atom-molecule benchmark, the eigenvalue problem is recast as a global matching system for projective solution lines; the infinite tail is represented as interval uncertainty in the terminal data, and a componentwise tail-robust Krawczyk-Brouwer inclusion supplies rigorous enclosures for a previously unresolved resonance pair. The work also documents both successful and failed AI-generated proof strategies, underscoring the necessity of human oversight for validated computation.

Significance. If the certificates hold, the manuscript supplies a reusable architecture for boundary-value problems with ill-conditioned propagation and uncertain asymptotics. It advances validated numerics in singular and non-normal settings while providing concrete evidence on the current limits of AI assistance in producing verifiable mathematical claims. The explicit treatment of an omitted componentwise check in an AI-generated argument is a constructive contribution to standards for AI-assisted verification.

major comments (1)
  1. [section describing the Krawczyk-Brouwer inclusion for the resonance pair] The enclosure of the resonance pair rests on the componentwise Krawczyk-Brouwer inclusion applied to the global matching system with tail uncertainty in a nonuniform polydisc. The abstract records that an AI-generated tail argument omitted the required componentwise check. The manuscript must explicitly demonstrate (in the section presenting the published certificate) that the radii are evaluated componentwise and that the inclusion theorem remains valid under the resulting nonuniformity; without this verification the ten-digit claim for each resonance is not guaranteed.
minor comments (2)
  1. Notation for the projective solution lines and the terminal data intervals would benefit from an additional clarifying sentence or small diagram.
  2. A few references to classical inclusion theorems (e.g., Krawczyk, Brouwer) appear only in the text; adding them to the bibliography would improve traceability.

Simulated Author's Rebuttal

1 responses · 0 unresolved

Thank you for the careful review and the recommendation of major revision. We appreciate the focus on ensuring the componentwise verification is explicit in the published certificate. We address the single major comment below and will revise the manuscript accordingly.

read point-by-point responses

  1. Referee: [section describing the Krawczyk-Brouwer inclusion for the resonance pair] The enclosure of the resonance pair rests on the componentwise Krawczyk-Brouwer inclusion applied to the global matching system with tail uncertainty in a nonuniform polydisc. The abstract records that an AI-generated tail argument omitted the required componentwise check. The manuscript must explicitly demonstrate (in the section presenting the published certificate) that the radii are evaluated componentwise and that the inclusion theorem remains valid under the resulting nonuniformity; without this verification the ten-digit claim for each resonance is not guaranteed.

    Authors: We agree that the componentwise evaluation must be shown explicitly for the published certificate. The global matching system uses a nonuniform polydisc to encode tail uncertainty, and the Krawczyk-Brouwer inclusion is applied componentwise. In the revised manuscript we will add a short dedicated paragraph (or subsection) immediately after the statement of the inclusion theorem. This paragraph will (i) record the componentwise radii computed from the interval data, (ii) verify the contraction mapping condition holds separately in each coordinate, and (iii) confirm that the standard Krawczyk-Brouwer theorem extends directly to the nonuniform case. The internal verification already performed shows the enclosures remain valid to ten digits; the added text will make this transparent without altering any numerical results. revision: yes

Circularity Check

0 steps flagged

No significant circularity; verification relies on external inclusion theorems

full rationale

The paper applies established methods (Dirichlet–Neumann bracketing, zero-counting, and componentwise Krawczyk–Brouwer inclusions) to certify numerical enclosures for two eigenvalue problems. The central non-normal result reformulates the problem as a global matching system with tail uncertainty encoded in projective data, then invokes a tail-robust inclusion theorem; the abstract explicitly flags and corrects an AI-generated omission of the componentwise check, indicating the published certificate is not self-referential. No equations reduce a claimed prediction or enclosure to a fitted parameter by construction, no load-bearing uniqueness theorem is imported via self-citation, and the derivation chain remains independent of the target results. This is a standard verified-computation workflow whose validity rests on external theorems rather than internal redefinition.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Based on the abstract alone, the work relies on standard numerical-analysis tools (Dirichlet-Neumann bracketing, Krawczyk-Brouwer theorem) without introducing new free parameters, ad-hoc axioms, or invented entities.

pith-pipeline@v0.9.1-grok · 5814 in / 1219 out tokens · 19719 ms · 2026-06-26T07:19:59.764525+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

29 extracted references

  1. [1]

    A. A. Abramov, A. Aslanyan, and E. B. Davies. Bounds on complex eigenvalues and resonances. Journal of Physics A: Mathematical and General, 34(1):57–72, 2001

    2001

  2. [2]

    Aguilar and J.-M

    J. Aguilar and J.-M. Combes. A class of analytic perturbations for one-body Schr¨ odinger Hamiltonians.Communications in Mathematical Physics, 22(4):269–279, 1971

    1971

  3. [3]

    Alper, M

    J. Alper, M. Barany, A. Chavarri Villarello, S. Dahmen, W. Dean, K. Ganapathy, M. Harris, D. Holmes, M. Jamnik, S. Kelk, B. Kra, U. Martin, B. Naskrecki, R. Ochigame, J. Portegies, and J. Schmitt. Leiden declaration on artificial intelligence and mathematics, 2026

    2026

  4. [4]

    J. J. Balmer. Notiz ¨ uber die Spectrallinien des Wasserstoffs.Annalen der Physik und Chemie, 261(5):80–87, 1885

  5. [5]

    Behrndt, P

    J. Behrndt, P. Schmitz, G. Teschl, and C. Trunk. Relative oscillation theory and essential spectra of Sturm–Liouville operators.Journal of Mathematical Analysis and Applications, 518(1):126673, 2023. 26M. J. COLBROOK

    2023

  6. [6]

    B¨ ogli, B

    S. B¨ ogli, B. M. Brown, M. Marletta, C. Tretter, and M. Wagenhofer. Guaranteed resonance enclosures and exclosures for atoms and molecules.Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences, 470(2171):20140488, 2014

    2014

  7. [7]

    N. Bohr. I. On the constitution of atoms and molecules.The London, Edinburgh, and Dublin Philosophical Magazine and Journal of Science, 26(151):1–25, 1913

    1913

  8. [8]

    B. M. Brown, M. Langer, M. Marletta, C. Tretter, and M. Wagenhofer. Eigenvalue bounds for the singular Sturm–Liouville problem with a complex potential.Journal of Physics A: Mathematical and General, 36(13):3773–3787, 2003

    2003

  9. [9]

    M. J. Colbrook.Infinite-Dimensional Spectral Computations: Foundations, Algorithms, and Modern Applications. Cambridge University Press, Cambridge, 2026

    2026

  10. [10]

    K. M. Collins, A. Q. Jiang, S. Frieder, L. Wong, M. Zilka, U. Bhatt, T. Lukasiewicz, Y. Wu, J. B. Tenenbaum, W. Hart, et al. Evaluating language models for mathematics through interactions.Proceedings of the National Academy of Sciences, 121(24):e2318124121, 2024

    2024

  11. [11]

    T. A. Driscoll, N. Hale, and L. N. Trefethen.Chebfun Guide. Pafnuty Publications, Oxford, 2014

    2014

  12. [12]

    Dyatlov and M

    S. Dyatlov and M. Zworski.Mathematical Theory of Scattering Resonances, volume 200 of Graduate Studies in Mathematics. American Mathematical Society, 2019

    2019

  13. [13]

    Gesztesy, B

    F. Gesztesy, B. Simon, and G. Teschl. Zeros of the Wronskian and renormalized oscillation theory.American Journal of Mathematics, 118(3):571–594, 1996

    1996

  14. [14]

    Hubert, R

    T. Hubert, R. Mehta, L. Sartran, M. Z. Horv´ ath, G. ˇZuˇ zi´ c, E. Wieser, A. Huang, J. Schrit- twieser, Y. Schroecker, H. Masoom, et al. Olympiad-level formal mathematical reasoning with reinforcement learning.Nature, pages 1–3, 2025

    2025

  15. [15]

    Johansson

    F. Johansson. Arb: Efficient arbitrary-precision midpoint-radius interval arithmetic.IEEE Transactions on Computers, 66(8):1281–1292, 2017

    2017

  16. [16]

    Krawczyk

    R. Krawczyk. Newton-Algorithmen zur Bestimmung von Nullstellen mit Fehlerschranken.Com- puting, 4(3):187–201, 1969

    1969

  17. [17]

    R. J. Lohner. Enclosing the solutions of ordinary initial and boundary value problems. InCom- puter Arithmetic: Scientific Computation and Programming Languages. B. G. Teubner, Stuttgart, 1987

    1987

  18. [18]

    R. E. Moore, R. B. Kearfott, and M. J. Cloud.Introduction to Interval Analysis. SIAM, Philadelphia, 2009

    2009

  19. [19]

    Neumaier.Interval Methods for Systems of Equations

    A. Neumaier.Interval Methods for Systems of Equations. Cambridge University Press, Cam- bridge, 1990

    1990

  20. [20]

    F. W. J. Olver, D. W. Lozier, R. F. Boisvert, and C. W. Clark, editors.NIST Handbook of Mathematical Functions. Cambridge University Press, 2010

    2010

  21. [21]

    Romera-Paredes, M

    B. Romera-Paredes, M. Barekatain, A. Novikov, M. Balog, M. P. Kumar, E. Dupont, F. J. Ruiz, J. S. Ellenberg, P. Wang, O. Fawzi, et al. Mathematical discoveries from program search with large language models.Nature, 625(7995):468–475, 2024

    2024

  22. [22]

    S. M. Rump. Verification methods: Rigorous results using floating-point arithmetic.Acta Numerica, 19:287–449, 2010

    2010

  23. [23]

    J. R. Rydberg. Recherches sur la constitution des spectres d’´ emission des ´ el´ ements chimiques. Kungliga Vetenskapsakademiens handlingar, 23(11):1–155, 1890

  24. [24]

    Schr¨ odinger

    E. Schr¨ odinger. Quantisierung als Eigenwertproblem.Annalen der Physik, 384(4):361–376, 1926

    1926

  25. [25]

    B. Simon. Resonances and complex scaling: A rigorous overview.International Journal of Quantum Chemistry, 14(4):529–542, 1978

    1978

  26. [26]

    G. Temple. The theory of Rayleigh’s principle as applied to continuous systems.Proceedings of the Royal Society of London, 119(782):276–293, 1928

    1928

  27. [27]

    Teschl.Mathematical Methods in Quantum Mechanics: With Applications to Schr¨ odinger Operators, volume 157 ofGraduate Studies in Mathematics

    G. Teschl.Mathematical Methods in Quantum Mechanics: With Applications to Schr¨ odinger Operators, volume 157 ofGraduate Studies in Mathematics. American Mathematical So- ciety, Providence, RI, 2 edition, 2014

    2014

  28. [28]

    Tucker.Validated Numerics: A Short Introduction to Rigorous Computations

    W. Tucker.Validated Numerics: A Short Introduction to Rigorous Computations. Princeton University Press, Princeton, NJ, 2011

    2011

  29. [29]

    M. Zworski. Mathematical study of scattering resonances.Bulletin of Mathematical Sciences, 7(1):1–85, 2017

    2017