Ten Digits on a Train: AI-Assisted Verification of Two Eigenvalue Problems
For researchers in numerical analysis and scientific computing, this work demonstrates a reusable architecture for certifying eigenvalues in ill-conditioned boundary-value problems, while also exposing the limitations of AI in rigorous mathematical verification.
The paper presents a human-AI collaboration that certifies eigenvalues of a singular Schrödinger operator and a non-normal atom-molecule benchmark to ten decimal places, using a novel global matching system and tail-robust inclusion. The AI generated accurate candidates and proof strategies, but several failed, highlighting the need for human judgment in validated computation.
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ödinger 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.