Auditing an AI-Generated Mathematical Proof: A Correction to a Greedy Conditioning Lemma in Quantum Parallel Repetition

• URL: http://arxiv.org/abs/2608.14673v1
• Date: Mon, 03 Aug 2026 15:12:46 GMT
• Title: Auditing an AI-Generated Mathematical Proof: A Correction to a Greedy Conditioning Lemma in Quantum Parallel Repetition
• Abstract summary: This note gives an explicit counterexample, identifies the intended continuation condition, and supplies a complete corrected proof.<n>It should not, however, be read as an independent verification of the main parallel-repetition theorem.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Chapter 6 of OpenAI's *Ten Advances in Mathematics and Theoretical Computer Science* claims an exponential parallel-repetition theorem for all finite two-player, one-round entangled games. Early in the proof, the chapter uses a quantitative greedy conditioning lemma. The lemma is meant to select a small set of coordinates (D) such that, after conditioning on winning every coordinate in (D), a randomly chosen remaining coordinate is won with average probability at least (1-δ). The statement is correct, but the proof as printed contains a polarity error. Its continuation test is written in terms of average success, while the next step requires a coordinate with a large conditional failure probability. That implication is false, and even simple examples can leave the printed procedure without a valid next move. This note gives an explicit counterexample, identifies the intended continuation condition, and supplies a complete corrected proof. The repair is local: it leaves the statement of the lemma and the parameters used later in the chapter unchanged. It should not, however, be read as an independent verification of the main parallel-repetition theorem. More broadly, the example shows how a mathematically plausible AI-generated argument can hide a small but decisive reversal between complementary events.

Related papers

• Trust the Spec, Not the Code - A Specification-First, AI-Assisted Case Study in Online Banking [1.6796354350132203]
  Formal specification promises early error detection, explicit invariants, and correctness by design, yet its notational cost has kept it out of mainstream practice.<n>We argue that AI can serve as an intermediate specification language that is precise enough to reason over and prove.<n>The specification becomes the artifact one authors, reviews, proves, and refines; the code becomes regenerable output.
  arXiv  Detail & Related papers  (2026-09-07T11:35:49Z)
• The Condition-Number Barrier in Sparse Least Squares [77.64108812086542]
  In [AS21], Axiotis and Sviridenko conjectured that the linear dependence on the restricted condition number in convex optimization cannot be improved by a sparse-time algorithm.<n>We establish their conjectured lower bound for least-squares objectives, conditional on the randomized exact-volume Small-Set Expansion Hypothesis.
  arXiv  Detail & Related papers  (2026-08-03T17:57:01Z)
• The Time-Space Complexity of Checking Multiple Assertions in Quantum Programs [0.5524804393257919]
  checking a quantum program that contains multiple assertions often requires using additional space or running the program additional times.<n>For a program with $n$ assertions, a naive strategy uses $n$ ancillas to learn all $n$ outcomes.<n>An alternative uses one ancilla but repeats program execution over $n$ rounds, checking one assertion per round.
  arXiv  Detail & Related papers  (2026-07-13T15:09:04Z)
• Ten Digits on a Train: AI-Assisted Verification of Two Eigenvalue Problems [0.0]
  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.
  arXiv  Detail & Related papers  (2026-06-22T18:03:59Z)
• LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization [104.06650149974585]
  We present LeanMarathon, a multi-agent harness for reliable research-level Lean autoformalization.<n>Four contract-scoped agents construct, audit, prove, and repair this blueprint.<n>We evaluate LeanMarathon on two recent research papers spanning four Erds problems.
  arXiv  Detail & Related papers  (2026-06-03T20:09:39Z)
• Yanasse: Finding New Proofs from Deep Vision's Analogies, Part 1 [51.56484100374058]
  System extracts tactic usage distributions across 27 top-level areas of Mathlib.<n>It computes z-scores to identify tactics that are heavily used in a source area but rare or absent in a target area.<n>It matches source and target proof states via GPU-accelerated NP-hard analogy.
  arXiv  Detail & Related papers  (2026-04-19T03:27:16Z)
• A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem [0.0]
  Rice's theorem states that no non-trivial semantic property of programs is decidable.<n>We present a proof that is constructive relative to the undecidability of Hilbert's Tenth Problem (MRDP)<n>The argument is structured as two separate implications, never asserting a disjunction about solvability, and never examining P(bot)
  arXiv  Detail & Related papers  (2026-04-11T20:45:58Z)
• The Aldous--Lyons Conjecture II: Undecidability [3.8370118222043694]
  We show that given a tailored non-local game $G$, it is undecidable to distinguish between the case where $G$ has a special kind of perfect strategy, and the case where every strategy for $G$ is far from being perfect.<n>Using a reduction introduced in the companion paper [BCLV24], this undecidability result implies a negative answer to the Aldous--Lyons conjecture.
  arXiv  Detail & Related papers  (2024-12-30T22:59:56Z)
• Some consequences of Sica's approach to Bell's inequalities [55.2480439325792]
  Louis Sica derived Bell's inequalities from the hypothesis that the time series of outcomes observed in one station does not change if the setting in the other station is changed. In this paper, Sica's approach is extended to series with non ideal efficiency and to the actual time structure of experimental data.
  arXiv  Detail & Related papers  (2024-03-05T13:59:52Z)
• Global Nash Equilibrium in Non-convex Multi-player Game: Theory and Algorithms [66.8634598612777]
  We show that Nash equilibrium (NE) is acceptable to all players in a multi-player game. We also show that no one can benefit unilaterally from the general theory step by step.
  arXiv  Detail & Related papers  (2023-01-19T11:36:50Z)
• Connes implies Tsirelson: a simple proof [91.3755431537592]
  We show that the Connes embedding problem implies the synchronous Tsirelson conjecture. We also give a different construction of Connes' algebra $mathcalRomega$ appearing in the Connes embedding problem.
  arXiv  Detail & Related papers  (2022-09-16T13:59:42Z)
• multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
  We focus on a type of linguistic formal reasoning where the goal is to reason over explicit knowledge in the form of natural language facts and rules. A recent work, named PRover, performs such reasoning by answering a question and also generating a proof graph that explains the answer. In our work, we address a new and challenging problem of generating multiple proof graphs for reasoning over natural language rule-bases.
  arXiv  Detail & Related papers  (2021-06-02T17:58:35Z)

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.