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

• URL: http://arxiv.org/abs/2606.23821v1
• Date: Mon, 22 Jun 2026 18:03:59 GMT
• Title: Ten Digits on a Train: AI-Assisted Verification of Two Eigenvalue Problems
• Abstract summary: This article reports a human--AI collaboration on two such computations.<n>For a singular self-adjoint Schrdinger operator, a verified zero count and Dirichlet--Neumann bracketing certify the complete negative spectrum to ten decimal places.<n>For a delicate non-normal atom--molecule benchmark, a previously unresolved resonance pair is separated, with each member enclosed to ten digits.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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ö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.

Related papers

• AI Grinding for Fun and Cryptanalysis [0.0]
  We present an autonomous cryptanalysis workflow in which agents generate, test, and refine hypotheses before human review.<n>First, a public map or input representation erases or exposes a relation that a construction must hide.<n>Second, a simulator, error law, or parameter certification uses a distribution different from the one claimed.
  arXiv  Detail & Related papers  (2026-08-22T14:37:46Z)
• Characterizing initial human-AI proof formalization workflows [66.06866890889131]
  Advances in AI systems' ability to generate code and engage in increasingly high-level mathematical reasoning promise to transform people's ability to formalize and thereby verify proofs.<n>We conduct a mixed-methods analysis into the initial impact of AI on people's formalization.<n>A qualitative survey shows that people's preferences are diverse, but with a general desire for AI assistance in formalization.
  arXiv  Detail & Related papers  (2026-06-02T22:58:19Z)
• The Deterministic Horizon: Impossibility Results as Design Specifications for Trustworthy AI Systems [0.0]
  This thesis turns impossibility results from curiosities into design rules.<n>Its flagship result proves an accuracy ceiling set by architecture alone.<n>The same argument recasts across subfields.
  arXiv  Detail & Related papers  (2026-05-21T20:48:35Z)
• The Specification as Quality Gate: Three Hypotheses on AI-Assisted Code Review [0.0]
  The dominant industry response to AI-generated code quality problems is to deploy AI reviewers.<n>This paper argues that this response is structurally circular when executable specifications are absent.
  arXiv  Detail & Related papers  (2026-03-26T11:59:05Z)
• Benchmarking Fraud Detectors on Private Graph Data [70.4654745317714]
  Currently, many types of fraud are managed in part by automated detection algorithms that operate over graphs.<n>We consider the scenario where a data holder wishes to outsource development of fraud detectors to third parties.<n>Third parties submit their fraud detectors to the data holder, who evaluates these algorithms on a private dataset and then publicly communicates the results.<n>We propose a realistic privacy attack on this system that allows an adversary to de-anonymize individuals' data based only on the evaluation results.
  arXiv  Detail & Related papers  (2025-07-30T03:20:15Z)
• Solving Inequality Proofs with Large Language Models [42.667163027148916]
  Inequality proving is crucial across diverse scientific and mathematical fields.<n>This makes it a demanding frontier for large language models (LLMs)<n>We release IneqMath, an expert-curated dataset of Olympiad-level inequalities.
  arXiv  Detail & Related papers  (2025-06-09T16:43:38Z)
• Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities [46.111273938884295]
  We study provers' ability to recognize that the given problem simplifies by applying a known inequality such as AM/GM.<n>Although these problems remain easy for humans, we find that most provers -- including Goedel, rewriting, and Kimina-7B -- struggle significantly.<n>Our results expose a persisting gap between the behavior of current AI provers and human intuition.
  arXiv  Detail & Related papers  (2025-05-19T03:56:05Z)
• Validation tests of GBS quantum computers give evidence for quantum advantage with a decoherent target [62.997667081978825]
  We use positive-P phase-space simulations of grouped count probabilities as a fingerprint for verifying multi-mode data. We show how one can disprove faked data, and apply this to a classical count algorithm.
  arXiv  Detail & Related papers  (2022-11-07T12:00:45Z)
• Complexity-Theoretic Limitations on Quantum Algorithms for Topological Data Analysis [59.545114016224254]
  Quantum algorithms for topological data analysis seem to provide an exponential advantage over the best classical approach. We show that the central task of TDA -- estimating Betti numbers -- is intractable even for quantum computers. We argue that an exponential quantum advantage can be recovered if the input data is given as a specification of simplices.
  arXiv  Detail & Related papers  (2022-09-28T17:53:25Z)
• Neuro-Symbolic Entropy Regularization [78.16196949641079]
  In structured prediction, the goal is to jointly predict many output variables that together encode a structured object. One approach -- entropy regularization -- posits that decision boundaries should lie in low-probability regions. We propose a loss, neuro-symbolic entropy regularization, that encourages the model to confidently predict a valid object.
  arXiv  Detail & Related papers  (2022-01-25T06:23:10Z)
• Doubly-Valid/Doubly-Sharp Sensitivity Analysis for Causal Inference with Unmeasured Confounding [62.40420028973522]
  We study the problem of constructing bounds on the average treatment effect in the presence of unobserved confounding. We propose novel estimators of these bounds that we call "doubly-valid/doubly-sharp" (DVDS) estimators.
  arXiv  Detail & Related papers  (2021-12-21T18:55:12Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.