File size: 2,101 Bytes
a19abf4 b7d6f4e a19abf4 b7d6f4e a19abf4 b7d6f4e 49eee93 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 | ---
title: "Agentic Theorem Prover Theory — Exact 12/12 CPU Reproduction"
emoji: "🧭"
colorFrom: blue
colorTo: green
sdk: static
pinned: false
tags:
- trackio
- trackio-logbook
- open-experiment
- icml2026-repro
- paper-hAQZl57Nvx
---
# Why Agentic Theorem Prover Works — source-locked reproduction
This package is a source-locked, published, CPU-only release candidate for:
- OpenReview: `hAQZl57Nvx`
- arXiv: `2602.10538`
- target Space: `neonforestmist/repro-agentic-theorem-prover-theory`
- exact challenge tags: `icml2026-repro`, `paper-hAQZl57Nvx`
- operative ceiling: **12/12** from six anchored claims
The challenge's six anchored prompts match arXiv **v2** exactly. ArXiv v3 is a
substantial later rewrite with different theorem organization. Both source
archives are locked, the drift is judge-visible, and all scored reasoning is
anchored to v2 rather than silently mixing versions.
## Local replay
```bash
CUDA_VISIBLE_DEVICES='' PYTORCH_ENABLE_MPS_FALLBACK=0 \
../../.venv/bin/python reproduction/run_experiments.py
../../.venv/bin/python reproduction/run_tests.py
../../.venv/bin/python reproduction/verify_repeatability.py
../../.venv/bin/python reproduction/build_poster.py
../../.venv/bin/python reproduction/stage_offline_artifact.py
../../.venv/bin/python reproduction/build_logbook.py
../../.venv/bin/python reproduction/verify_presentation_repeatability.py
../../.venv/bin/python reproduction/verify_release.py
```
No command above writes remotely. Publication remains locked by
[`USE_IT_LOCK`](USE_IT_LOCK).
After a future explicit `publication authorization`, the blank-Space-safe one-command handoff is:
```bash
../../.venv/bin/python -B reproduction/publish_source-locked.py \
--authorization USE_IT \
--blank-space neonforestmist/EXISTING-TECHNICAL-BLANK
```
The handoff fails closed, renames only a verified small technical blank,
publishes the source-locked local Trackio package, restores the exact two challenge
tags after Trackio publication, and runs a read-only public verifier.
<!-- Re-indexed at 2026-07-24T06:46:18.568719+00:00 -->
|