VGPT-RSI for RH-Adjacent Formal Progress: Boundary Certificates, Verified Finite Lagarias Inequalities, and Explicit Failure Localization

• URL: http://arxiv.org/abs/2606.15096v1
• Date: Sat, 13 Jun 2026 04:12:25 GMT
• Title: VGPT-RSI for RH-Adjacent Formal Progress: Boundary Certificates, Verified Finite Lagarias Inequalities, and Explicit Failure Localization
• Abstract summary: We apply Verifiable Growing Physical Transformer with Recursive Self-Improvement to two RH-adjacent certification tasks.<n>First, we construct and verify a finite RH-boundary certificate for inequality on a parameterized safe lower curve over a region.<n>Second, we initiate a formal Lagarias-route certificate. Lagarias criterion states that RH is equivalent to the global inequality.
• Score: 4.067416725742151
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: The Riemann Hypothesis remains one of the central unsolved problems in mathematics. Rather than claiming proof, we investigate whether a verifiable AI-assisted reasoning system can produce reliable, formally checked partial progress while explicitly identifying the remaining mathematical obstructions. We apply the Verifiable Growing Physical Transformer with Recursive Self-Improvement (VGPT-RSI) to two RH-adjacent certification tasks. First, we construct and verify a finite RH-boundary certificate for inequality on a parameterized safe lower curve over a region. The numerical boundary curve is converted into a certificate-backed lower curve, audited using outward-rounded interval arithmetic and Arb/FLINT ball arithmetic, and then checked in Rocq/CoqInterval for the parameterized theorem. Second, we initiate a formal Lagarias-route certificate. Lagarias criterion states that RH is equivalent to the global inequality. We formalize the finite quantity and produce a Coq-checked finite certificate. The final system identifies the exact unresolved mathematical bottlenecks: formalizing the Lagarias equivalence, proving the global tail theorem beyond any finite cutoff, and potentially reducing counterexamples to colossally abundant or related extremal integers. These results demonstrate that VGPT-RSI can produce certified RH-adjacent formal progress, organize proof dependencies, and avoid overclaiming when the remaining obstruction is genuinely mathematical.

Related papers

• A Reference-Free Score for Detecting Silent Reasoning Failures in Large Language Models [1.0602247913671219]
  Reasoning Answer Faithfulness Score (RAFS) is a reference free, instance level diagnostic of whether an emitted mathematical trace is locally credible.<n>RAFS combines step validity, reasoning to answer entailment and counterfactual sensitivity, answer consensus, and conditional reasoning stability.<n>RAFS is intended to complement mathematical answer accuracy with an auditable warning signal for silent reasoning failures and answer extraction errors.
  arXiv  Detail & Related papers  (2026-07-28T07:28:38Z)
• Domain-Validity-Gated Metamorphic Testing of Scientific ML Surrogates [6.691613382732758]
  We study how candidate metamorphic relations can be screened for domain validity and turned into executable test assets for SciML surrogates.<n>We propose a domain-validity that admits a candidate only when its tolerance dominates the operator's numerical floor and its preconditions hold.<n>The evidence spans two CFD tasks and a second PDE family, supporting a validity-aware bridge from candidate MRs to auditable SciML test assets.
  arXiv  Detail & Related papers  (2026-06-16T05:13:05Z)
• Finite Certificates for In-Context Determinacy and a Threshold Theory of Emergence in Language Models [0.2864713389096699]
  This paper develops a model-theoretic framework for verifying context-conditioned language-model behavior.<n>It provides finite context certificates, pair-separator hitting sets, query teaching dimension, prompt-preservation criteria, and scale-limit witnesses.
  arXiv  Detail & Related papers  (2026-05-30T14:07:58Z)
• Value Functions as Supermartingale Certificates [48.922124609307566]
  We show that under an appropriate reward, the value function associated to a policy that almost surely satisfies an $$-regular property encodes a Streett supermartingale certificate for that specification.<n>Our results, validated experimentally on finite Markov decision processes, hold for finite, countably infinite, and continuous state spaces, suggesting a principled route to certificate synthesis via RL.
  arXiv  Detail & Related papers  (2026-05-29T16:39:02Z)
• Formally Verified Patent Analysis via Dependent Type Theory: Machine-Checkable Certificates from a Hybrid AI + Lean 4 Pipeline [0.0]
  We present a formally verified framework for patent analysis as a hybrid AI + Lean 4 pipeline.<n>The DAG-coverage core (Algorithm 1b) is fully machine-verified once bounded match scores are fixed.<n>Claims are encoded as DAGs in Lean 4, match strengths as elements of a verified complete lattice, and confidence scores propagate through dependencies via proven-correct monotone functions.
  arXiv  Detail & Related papers  (2026-04-20T22:02:57Z)
• Exact Structural Abstraction and Tractability Limits [0.0]
  Exact correctness depends only on the induced classes $s sim_R simation' iff mathrmAdm_R(s)$.<n>Decision, search, approximation, statistical, randomized horizon, and distributional guarantees all reduce to this same quotient-recovery problem.
  arXiv  Detail & Related papers  (2026-04-08T17:59:47Z)
• 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)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheorem is a comprehensive informal theorem-proving framework exploiting natural language to enhance mathematical reasoning.<n>DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs.<n>We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference.
  arXiv  Detail & Related papers  (2025-05-29T17:59:39Z)
• Latent Veracity Inference for Identifying Errors in Stepwise Reasoning [78.29317733206643]
  We introduce Veracity Search (VS), a discrete search algorithm over veracity assignments.<n>It performs otherwise intractable inference in the posterior distribution over latent veracity values.<n>It generalizes VS, enabling accurate zero-shot veracity inference in novel contexts.
  arXiv  Detail & Related papers  (2025-05-17T04:16:36Z)
• Proving Theorems Recursively [80.42431358105482]
  We propose POETRY, which proves theorems in a level-by-level manner. Unlike previous step-by-step methods, POETRY searches for a sketch of the proof at each level. We observe a substantial increase in the maximum proof length found by POETRY, from 10 to 26.
  arXiv  Detail & Related papers  (2024-05-23T10:35:08Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARD is a framework that masters uniform synthesis of theorem and proof data of high quality and diversity. We present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points. We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data.
  arXiv  Detail & Related papers  (2024-02-14T05:57:58Z)
• Towards Evading the Limits of Randomized Smoothing: A Theoretical Analysis [74.85187027051879]
  We show that it is possible to approximate the optimal certificate with arbitrary precision, by probing the decision boundary with several noise distributions. This result fosters further research on classifier-specific certification and demonstrates that randomized smoothing is still worth investigating.
  arXiv  Detail & Related papers  (2022-06-03T17:48:54Z)

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.