04 — Exact claims, source versions, and falsifiers
Exact official claim surface
The six scoring-operative anchored claims are repeated verbatim:
Theorem 1 establishes that the space of finite measures with bounded mass forms a compact metric space under the bounded Lipschitz metric, providing the topological foundation for the measure-valued goal encoding of the reachability MDP (Theorem 1, Section 3).
Theorem 2 proves that under mild Feller-type continuity conditions on the transition kernel, optimal deterministic Markov policies exist for the finite-horizon time-bounded reachability MDP (Theorem 2).
Theorem 3 shows that sequences of functions satisfying Bellman sub-/super-solution inequalities yield provability certificates (upper and lower bounds on the optimal value function) without requiring the full MDP to be solved, with the certificate gap defined as UB(x0) - LB(x0) (Theorem 3, Definition 5, Section 5).
Theorem 4 bounds the worst-case regret of score-guided planning under uniform score-approximation error εb as 0 ≤ V*_B(x0) - V^{πh}B(x0) ≤ 2∑{b=1}^{B} εb, showing performance degrades linearly with accumulated approximation error (Theorem 4, Section 6).
Theorem 5 shows that under a margin condition on action-value separation, the expected regret improves to O(Bε^{β+1}) for β>0, i.e., faster than the worst-case linear-in-B rate of Theorem 4 (Theorem 5).
Theorem 6 derives a high-probability estimation-error bound of order O(L H d_D/(d_D+2) (log(n/δ)/n)^{1/(d_D+2)}) under a doubling-dimension assumption on the relevant problem domain, formalizing how statistical complexity of a biased real-world problem distribution governs sample efficiency (Theorem 6, Section 7).
For provenance, the legacy three-claim base layer is also retained verbatim:
- Proves existence of optimal policies under mild regularity using Bellman structure in time-bounded reachability MDPs
- Derives provability certificates via sub-/super-solution inequalities and bounds performance gap of score-guided planning in terms of approximation error and sequential statistical complexity
- Provides principled component-sensitive explanation of when agentic theorem provers succeed on biased real-world problem distributions
Version lock
- OpenReview:
hAQZl57Nvx; arXiv:2602.10538 - v2 PDF SHA-256:
b725e91c0cfe924e6aa536d34fbde4da905003a3dfc94b65b7c7c050d6b1a9ad - v2 source SHA-256:
ffd5a325a9f10e60635b7b36a38a8c0dd6dad9a3063eaf5c0134c0bf2d3fb0f6 - v3 source SHA-256:
ba30962d80ae1725cccd6e2fdba44abdf94485dd63ffb5081e2e5666af6abd9e - v2 theory TeX SHA-256:
8d06629c1f87a8409e449b6c11b8d0ced99feefa3e97d38cf407353525e9fcc2 - target:
neonforestmist/repro-agentic-theorem-prover-theory - tags:
icml2026-repro,paper-hAQZl57Nvx
All six numbered labels are present in v2 and absent in v3. This is not a contradiction: v3 is a later rewrite, and its revised abstract centers faithful state abstraction and occupancy-weighted offline regression. Because the challenge text was generated from v2, v2 is the decisive source for scoring. v3 is retained to expose drift and prevent accidental source mixing.
At the read-only lock, the author Space listing contained neither the exact target nor paper-hAQZl57Nvx; the official verdict snapshot contained no matching target or OpenReview ID. No competitor file was opened.
Destructive controls
| mutation | outcome | witness |
|---|---|---|
use_v3_as_numbered_source |
killed | v3 lacks all six v2 labels |
drop_compactness |
killed | Theorem 2 assumption gate |
drop_feller_continuity |
killed | Theorem 2 assumption gate |
replace_supremum_by_average |
killed | Bellman identity mismatch |
reverse_subsolution_inequality |
killed | exact lower-certificate gate |
reverse_supersolution_inequality |
killed | exact upper-certificate gate |
omit_certificate_gap |
killed | judge-visible Definition 5 gate |
use_one_epsilon_regret |
killed | tight factor-two witness |
sum_only_last_depth_error |
killed | multi-depth exact regret gate |
linear_margin_rate |
killed | quadratic beta=1 witness |
wrong_margin_exponent |
killed | log-log slope gate |
dimension_free_rate |
killed | dimension sensitivity |
omit_approximation_error |
killed | additive expressivity gate |
claim_finite_sweep_is_universal_proof |
killed | scope-language gate |
wrong_paper_tag |
killed | exact tag gate |
All 15/15 controls are killed. They reject the wrong source version, missing compactness/Feller assumptions, a mean in place of the Bellman supremum, reversed certificate inequalities, an omitted certificate gap, a false factor-one regret claim, dropped depth errors, a linearized margin rate, the wrong margin exponent, a dimension-free statistical rate, missing approximation error, a finite-sweep universal-proof claim, and the wrong paper tag.
No source-reported empirical benchmark is presented as rerun. The decisive evidence is theorem-source identity plus exact operational certificates. This separation keeps theoretical replication strong without manufacturing a GPU experiment the paper does not require.