docs: record authorized runner root filesystem expansion

Reviewed-on: #7

.gitea/workflows/env-probe.yml

@@ -29,3 +29,20 @@ jobs:
           (find / -maxdepth 4 \( -name 'lake-manifest.json' -o -name '.lake' \) -not -path '/proc/*' 2>/dev/null | head -20) || true
           (docker images 2>&1 | head -20) || true
           (docker ps -a 2>&1 | head -10) || true
+      - name: Read-only storage diagnosis
+        run: |
+          set -eu
+          hostname
+          lsblk -e 7 -o NAME,PATH,SIZE,FSTYPE,MOUNTPOINTS
+          findmnt -T /var/lib/docker
+          df -hT / /var/lib/docker
+          docker info --format 'storage={{.Driver}} root={{.DockerRootDir}}'
+          docker system df
+          docker builder du 2>/dev/null || true
+          for dir in /var/lib/docker /var/lib/containerd /opt/lean-cache /var/cache /tmp /var/log; do
+            if [ -d "$dir" ]; then du -xhd1 "$dir" 2>/dev/null || true; fi
+          done
+          for tool in sfdisk growpart resize2fs xfs_growfs; do command -v "$tool" || true; done
+          if [ "$(hostname)" = "iZ6we8b3jgd6nc2qehu06lZ" ] && command -v growpart >/dev/null; then
+            growpart -N /dev/nvme0n1 3 || true
+          fi

.gitea/workflows/runner-storage-maintenance.yml

@@ -0,0 +1,49 @@
+name: runner-storage-maintenance
+
+# Manual-only. Never runs on push or pull_request.
+on:
+  workflow_dispatch:
+    inputs:
+      confirm:
+        description: Enter EXPAND_RUNNER_ROOT after owner approval
+        required: true
+        type: string
+
+jobs:
+  expand-root:
+    if: ${{ github.event_name == 'workflow_dispatch' && inputs.confirm == 'EXPAND_RUNNER_ROOT' }}
+    runs-on: ubuntu24.04-x64-lean4.35
+    timeout-minutes: 20
+    steps:
+      - name: Back up partition table and expand the authorized ext4 root
+        run: |
+          # Owner-authorized manual-only root partition/filesystem expansion.
+          set -euo pipefail
+          exec 9>/var/lock/lean-bench-root-maintenance.lock
+          flock -n 9
+          [ "$(hostname)" = "iZ6we8b3jgd6nc2qehu06lZ" ]
+          [ "$(id -u)" = 0 ]
+          [ "$(blkid -s PARTUUID -o value /dev/nvme0n1p3 | tr A-Z a-z)" = 9b694bad-5bbb-4485-860f-e5544ae47410 ]
+          [ "$(findmnt -n -o SOURCE /)" = /dev/nvme0n1p3 ]
+          [ "$(findmnt -n -o FSTYPE /)" = ext4 ]
+          [ "$(lsblk -n -o START /dev/nvme0n1p3 | tr -d ' ')" = 413696 ]
+          [ "$(blockdev --getsize64 /dev/nvme0n1)" -ge 161061273600 ]
+          backup_dir="/root/lean-bench-maintenance/$(date -u +%Y%m%dT%H%M%SZ)"
+          install -d -m 700 "$backup_dir"
+          sfdisk --dump /dev/nvme0n1 > "$backup_dir/nvme0n1.sfdisk"
+          sync
+          printf 'Partition-table backup: %s\n' "$backup_dir/nvme0n1.sfdisk"
+          set +e
+          growpart -N /dev/nvme0n1 3 > "$backup_dir/growpart-dry-run.log" 2>&1
+          probe_status=$?
+          set -e
+          if [ "$probe_status" = 0 ]; then
+            growpart /dev/nvme0n1 3
+          elif ! grep -q '^NOCHANGE:' "$backup_dir/growpart-dry-run.log"; then
+            cat "$backup_dir/growpart-dry-run.log"
+            exit "$probe_status"
+          fi
+          resize2fs /dev/nvme0n1p3
+          [ "$(lsblk -n -o START /dev/nvme0n1p3 | tr -d ' ')" = 413696 ]
+          lsblk -e 7 -o NAME,PATH,SIZE,FSTYPE,MOUNTPOINTS
+          df -hT / /var/lib/docker

.gitignore

@@ -38,8 +38,11 @@ htmlcov/
 .idea/
 .vscode/
 
-# Local experiment data: passages from copyrighted books and per-run outputs
+# Local experiment data: passages from copyrighted books and per-run outputs.
+# Each experiment keeps raw data in experiments/<ID>/data/ (ignored) and small,
+# text-free artifacts (keys, verdict-only labels, summaries) in labels/ and results/ (tracked).
 runs/
-**/private/
-*.labels.json
 .leanbench-cache/
+# (data/ above already covers experiments/*/data/; results/ above is ignored for the
+# pipeline's own output, but experiment summaries are numbers only and are tracked.)
+!experiments/*/results/

README.md

@@ -272,6 +272,10 @@ The paper plan for this project (ACL 2027 target, ARR deadline 4 Jan 2027) lives
 [`docs/TODO.md`](docs/TODO.md) and the acceptance-bar analysis in
 [`docs/acl-2027-bar.md`](docs/acl-2027-bar.md).
 
+Experiments have IDs (`P0`, `E0`-`E11`); the registry, phases, gates and conventions are in
+[`docs/experiments/README.md`](docs/experiments/README.md). CI runner and environment notes:
+[`docs/infrastructure/runner-lean435.md`](docs/infrastructure/runner-lean435.md).
+
 ## What this does not claim
 
 Lean says whether the code is *legal*, and — when there is a proof — whether it is

docs/experiments/P0-gpt-diagnostic.md

@@ -0,0 +1,127 @@
+# P0: full-cohort GPT-assisted diagnostic (2026-10-28)
+
+**All 65 items have a fresh source-role description, a fresh semantic judgment and a
+completed deterministic alignment. This is a same-assistant diagnostic, not an independent
+benchmark or a completion of the preregistered Qwen gate. No gate decision is issued.**
+
+## Scope and provenance
+
+The owner requested that the current GPT assistant reassess the entire cohort after the
+Qwen run was interrupted by provider billing failures. Every item was reviewed again;
+no Qwen detector output was reused, and the incomplete Qwen run was not patched with GPT
+outputs. The earlier labels and Qwen files remain unchanged in the original worktree.
+This branch starts at main `5d531c9` and does not depend on the separate billing-recovery PR.
+
+The source-role structures and four-way judgments were authored directly by the assistant
+in this chat, frozen before computing the new alignment statistics, and replayed by an
+offline script. They were not responses obtained through a GPT API endpoint. The exact
+deployed model identifier, temperature and chat token usage are unavailable; they are not
+invented. There were **zero new external model API calls** for this diagnostic, and no
+DashScope credential was loaded.
+
+The assistant had already seen the earlier labels, Lean code, detector implementation and
+aggregate compilation statistics. It also viewed passages and Lean together during this
+review. Thus the source descriptions are **not a blinded source-only extraction** and the
+new judgments are **not independent of the reference labels**. Reading only a passage when
+writing a role does not remove prior context exposure. Syntax and proof defects are
+separated from recoverable semantic meaning; no new Lean compilation or library API audit
+was performed. An independent human review remains necessary for research claims.
+
+## Results for all 65 items
+
+| Fresh semantic judgment | Items |
+|---|---:|
+| Faithful | 25 |
+| Minor drift | 13 |
+| Wrong | 24 |
+| Not formalizable from the extracted specification | 3 |
+| Total | 65 |
+
+The strict binary assistant judge flags every verdict except faithful. The full four-way
+judgment, error categories and an individual explanation are retained for every item.
+Explanations and role descriptions are private because they paraphrase the source passages.
+
+The unchanged deterministic role matcher flagged **55/65** items. It flagged all **24**
+items newly judged wrong, but also **16/25** newly judged faithful. These are comparisons
+between dependent components of the same diagnostic, not an independently measured recall
+or false-positive rate. They identify an over-sensitive diagnostic behavior worth auditing.
+
+Common conflict categories across all items include missing objects (41 items), degenerate
+projections (15), goal mismatch (15), missing hypotheses (14), extra hypotheses (13),
+quantifier conflicts (7) and type conflicts (5). Categories overlap. In particular, a named
+source quantity can be computed inline in Lean, a product representation can replace an
+abstract isomorphic group, and a bundled type can encode conditions without separate
+binders. The current lexical matcher does not establish equivalence of those representations.
+These are hypotheses for a later matcher audit, not measured causal explanations for every flag.
+No matching threshold, concept table or authored assessment was changed after the scores
+were inspected.
+
+## Relation to the frozen earlier AI labels
+
+The fresh four-way judgments agree with **59/65** earlier labels. Six changed:
+
+| Blind ID | Earlier AI label | Fresh judgment |
+|---|---|---|
+| P02 | Faithful | Minor drift |
+| P18 | Faithful | Minor drift |
+| P23 | Faithful | Minor drift |
+| P34 | Faithful | Minor drift |
+| P51 | Faithful | Minor drift |
+| P57 | Wrong | Minor drift |
+
+The six changes concern representation, type/scope and coverage judgments. They demonstrate
+annotation instability and should be independently adjudicated, not silently overwritten.
+The 59/65 agreement is **not an accuracy estimate**.
+
+For debugging continuity, the summary contains confusion counts and Wilson intervals against
+the frozen earlier AI labels. The primary comparison excludes earlier minor-drift and
+not-formalizable labels (55 items); the secondary comparison includes minor drift as positive
+(62 items). These tables are explicitly named `reference_agreement`. They cannot establish
+that GPT or role alignment outperforms Qwen. The Qwen coverage is incomplete and this pass
+has different provenance and no independent ground truth. `decision` is null; no GO,
+PARTIAL or NO-GO is computed.
+
+## Artifacts and replay
+
+Tracked, text-free artifacts:
+
+- `experiments/P0-pilot/results/gpt-diagnostic-summary.json`: provenance, input/assessment/code
+  hashes, distributions, fixed matching thresholds and non-independent agreement statistics.
+- `experiments/P0-pilot/results/gpt-diagnostic-items.json`: all 65 blind IDs, verdicts, error
+  categories, compile flags, role scores and conflict categories; no passages or explanations.
+- `experiments/P0-pilot/assistant_diagnostic.py`: validates authored inputs and replays the
+  existing projection, lint, alignment and statistics code offline.
+- `tests/test_assistant_diagnostic.py`: completeness, identity, schema, offline replay and
+  public-output privacy regressions using synthetic text.
+
+Private artifacts under the gitignored `experiments/P0-pilot/data/gpt-diagnostic/`:
+
+- `items.jsonl`: source-inclusive copy of the unchanged cohort.
+- `assistant-assessments.json`: all newly authored source structures and judgments, frozen
+  before alignment statistics were inspected.
+- `results.jsonl`: complete replay outputs for the 65 items.
+- `review.html`: local, self-contained per-item source/Lean/reason/role/alignment review.
+- `original-hashes.json`: snapshot of the earlier Qwen files and reference labels for
+  verifying that this work did not change them.
+
+Run from the repository root with the private files present:
+
+```sh
+PYTHONPATH=. python3 experiments/P0-pilot/assistant_diagnostic.py \
+  --items experiments/P0-pilot/data/gpt-diagnostic/items.jsonl \
+  --key experiments/P0-pilot/labels/key.json \
+  --assessments experiments/P0-pilot/data/gpt-diagnostic/assistant-assessments.json \
+  --labels experiments/P0-pilot/labels/labels.json \
+  --private-out experiments/P0-pilot/data/gpt-diagnostic \
+  --summary experiments/P0-pilot/results/gpt-diagnostic-summary.json \
+  --public-items experiments/P0-pilot/results/gpt-diagnostic-items.json
+```
+
+The replay is deterministic; it does not regenerate GPT judgments, call a model, or compile
+Lean. Without the private assessment file, public readers can inspect the categorical
+results but cannot reconstruct the authored descriptions and explanations from hashes.
+
+152 offline unit tests, repository-wide Ruff and diff checks passed locally without a Lean
+or Docker build. Remote Python and real Lean verification use the owner-confirmed
+`ubuntu24.04-x64-lean4.35` tag; the delivered PR records their current status. The existing
+PR workflow skips the Docker image job. No Phase 1 work has started.

docs/experiments/P0-pilot.md

@@ -1,11 +1,24 @@
-# Experiment protocol v1 (for approval)
+# P0: pilot protocol (v1)
 
-Status: **awaiting approval. No experiment has been run and no API spend has occurred.**
+Experiment ID **P0**, Phase 0. Registry and conventions: [README.md](README.md).
+
+Status: **approved 2026-10-22; 65 AI labels frozen 2026-10-28; detector execution pending explicit data-transfer approval. No pilot API request has been sent.**
+
+Owner amendment (2026-10-28, in the execution chat): Codex now handles preparation,
+annotation, detector execution and reporting; Kimi's participation is no longer required.
+The frozen labels are from one AI annotator, **not human ground truth**. The annotator saw
+the detector implementation and aggregate compile counts before labeling, but did not see
+per-item compiler outcomes or detector outputs. This departs from the original labeling plan;
+any resulting decision is provisional and cannot substitute for an independent human audit.
+Decision thresholds, detector prompts and the concept table remain fixed. Implementation
+repairs before the first paid call restore the complementary-signal PARTIAL rule, exclude
+minor drift from the primary wrong-versus-faithful comparison, enforce the cumulative HTTP
+request budget, and persist run identity and usage. See `experiments/P0-pilot/README.md`.
 Written 2026-10-22. Companion to `docs/research-plan.md` (what and why), `docs/TODO.md` (task list), `docs/acl-2027-bar.md` (bar). Target: ACL 2027 via ARR, deadline 4 Jan 2027 AoE.
 
-## 1. Decision requested
+## 1. Decision (approved by the owner on 2026-10-22)
 
-Approve **Phase 0 (pilot)** now. It costs a few yuan of API calls, about 4 hours of one person's labeling time, and about 2 days elapsed. Its only job is to tell us whether the paper's central idea (role alignment) has signal before we spend six weeks and a large token budget on it. Phases 1-3 are described so you can see where this leads, but each needs its own go from you after the previous gate.
+**Phase 0 (pilot)** was approved. It costs a few yuan of API calls, about 4 hours of one person's labeling time, and about 2 days elapsed. Its only job is to tell us whether the paper's central idea (role alignment) has signal before we spend six weeks and a large token budget on it. Phases 1-3 are described so you can see where this leads, but each needs its own go from you after the previous gate.
 
 | Phase | What | Cost (API / people) | Elapsed | Gate to continue |
 |---|---|---|---|---|
@@ -20,11 +33,11 @@ Token and CPU figures are the plan's rough estimates (`research-plan.md` 7.9); t
 
 - **H1 (gap).** Compiling overstates fidelity: a large share of formalizations, compiled or not, do not say what the passage says.
 - **H3 (role alignment).** The deterministic alignment of the passage's roles against the Lean signature's roles flags unfaithful items better than the alternatives.
-- Phase 0 does *not* test H2, H4, H5 (guided formalization, retrieval, proving). They need Lean runs and more data.
+- P0 does *not* test H2 (repair), H4 (slot-constrained formalization) or H5 (schema-guided retrieval). They need Lean runs and more data (E8, E7, E9).
 
 ## 3. Phase 0 design
 
-**Items.** The 65 items in `runs/p85-110/items.jsonl` (pages 85-110 of one algebra text; 37 statements, 28 problems). Only 10 of them compiled in Lean. So the pilot judges *fidelity detection over all items*; it cannot yet say anything solid about "compiles but wrong" (n <= 10). That subset is reported with its interval but does not decide anything.
+**Items.** The 65 items in `experiments/P0-pilot/data/items.jsonl` (pages 85-110 of one algebra text; 37 statements, 28 problems). Only 10 of them compiled in Lean. So the pilot judges *fidelity detection over all items*; it cannot yet say anything solid about "compiles but wrong" (n <= 10). That subset is reported with its interval but does not decide anything.
 
 **Labels (ground truth).** One Lean-literate labeler (you, or someone you name) uses `labelsheet.html`: passage and Lean code side by side, shuffled, no compile status, no scores, no model output. Verdicts: faithful / minor drift / wrong / not formalizable, plus error types (missing or extra hypothesis, wrong type, quantifier, wrong conclusion, degenerate, hallucinated API). Labels are finished and saved before any detector output is opened. One labeler means no kappa in Phase 0; that is a stated limitation, fixed in Phase 1.
 
@@ -60,8 +73,8 @@ With about 65 items every interval is wide (a recall of 0.5 on 20 wrong items ha
 ## 5. Infrastructure (ready)
 
 - Runner `ubuntu24.04-x64-lean4.35`, Lean 4.35.0, Mathlib v4.35.0 cache, image `lean-bench:latest` kept on host; CI green on both repos.
-- Code on branch `exp/pilot-prep`: schema, projection, source-side extraction, alignment, lint, stats; labeling sheet, run and score scripts; 140 tests, ruff clean. Offline smoke of run -> score passes with a stub model.
-- Pilot data and labels stay local (`runs/`, `**/private/` are gitignored). The copyrighted book and text derived from it are never committed or released; the public release will use open-licensed books and hashes/spans only.
+- Code on `main`: schema, projection, source-side extraction, alignment, lint, stats; labeling sheet, run and score scripts; 140 tests, ruff clean. Offline smoke of run -> score passes with a stub model.
+- Raw pilot data stays local (`experiments/P0-pilot/data/` is gitignored); the blind key, the verdict-only labels and the numeric summary are tracked. The copyrighted book and text derived from it are never committed or released; the public release will use open-licensed books and hashes/spans only.
 
 ## 6. Risks specific to the near term
 

docs/experiments/README.md

@@ -0,0 +1,61 @@
+# Experiments
+
+Every experiment has one ID. The IDs `E0`-`E11` are the ones used in `docs/research-plan.md` section 6 and `docs/TODO.md`; `P0` is the pilot that gates them. Use the ID in commit messages, result files, and the paper's tables.
+
+Updated 2026-10-22.
+
+## Registry
+
+| ID | Name | Phase | Tests | Spec | Code | Status |
+|---|---|---|---|---|---|---|
+| **P0** | Pilot: do detectors find unfaithful items on the 65 existing ones? | 0 | early look at H1, H3 | [P0-pilot.md](P0-pilot.md) | `experiments/P0-pilot/` | Ready. Waiting on approval record and the 65 human labels. No run yet. |
+| E0 | Simplex projection validated against manual parse (>= 95% on >= 100 signatures) | 1 | method check for C1 | research-plan 6, E0 | `leanbench/project.py`, `tests/test_project.py` | Code done and unit-tested; manual-parse check not done |
+| E1 | Corpus and benchmark construction (6-8 books, >= 1,500 items) | 1 | enables all | research-plan 6, E1 | not written | Not started |
+| E2 | Detection quality (P/R/F1, boundary IoU, run-to-run Jaccard) | 2 | none (measurement) | research-plan 6, E2 | not written | Not started |
+| E3 | Extraction / OCR comparison | 2 | none (measurement) | research-plan 6, E3 | not written | Not started |
+| E4 | Compile vs. faithful gap across >= 4 models | 2 | H1 | research-plan 6, E4 | not written | Not started |
+| E5 | Human annotation: 600-item core, kappa on 200 overlap | 2 | enables E4, E6 | research-plan 6, E5 | `experiments/P0-pilot/make_sheet.py` is the prototype | Not started |
+| E6 | Role-alignment fidelity filter vs. baselines (main method) | 2 | H3 | research-plan 6, E6 | `leanbench/align.py`, `lint.py`, `evalstats.py` | Method code done; P0 is its first check |
+| E7 | Slot-constrained vs. free-form formalization | 2 | H4 | research-plan 6, E7 | not written | Not started |
+| E8 | Repair ablation (0/1/3/5 attempts, whole vs. slot-level) | 2 | H2 | research-plan 6, E8 | not written | Not started |
+| E9 | Schema-guided retrieval and proof guidance | 3 | H5 | research-plan 6, E9 | not written | Not started |
+| E10 | Contamination check | 3 | none (control) | research-plan 6, E10 | not written | Not started |
+| E11 | Cost, time, reliability | 3 | none (report) | research-plan 6, E11 | not written | Not started |
+
+Hypotheses (H1-H5) are stated in `docs/research-plan.md` section 2: H1 compile rate overstates fidelity; H2 repair raises compile more than fidelity; H3 role alignment catches wrong-but-compiles items; H4 slot-constrained formalization raises fidelity; H5 schema-guided retrieval helps provers.
+
+## Phases and gates
+
+| Phase | Experiments | Cost | Elapsed | Gate to continue |
+|---|---|---|---|---|
+| 0 | P0 | ~200 API calls, ~4 h of one labeler | ~2 days | decision rule in P0-pilot.md |
+| 1 | E0, E1, annotation guideline and 50-item kappa pilot | ~10-20M tokens, 2 annotators ~15 h each | ~2 weeks | kappa >= 0.6; E0 >= 95% |
+| 2 | E2-E8 | ~135M tokens plus judges, 2 annotators ~60 h total | 3-4 weeks | go/no-go on 8 Dec |
+| 3 | E9-E11 | bounded by time left | to 24 Dec | tables frozen 24 Dec |
+
+Each phase needs its own go from the project owner. Token and CPU figures are the plan's rough estimates (research-plan 7.9) and are recomputed from P0 before Phase 1.
+
+## Conventions
+
+**Layout.** One directory per experiment: `experiments/<ID>-<slug>/` with
+
+- `README.md`: the commands, in order
+- scripts
+- `data/`: raw inputs and outputs. **Gitignored.** Anything with passages from a copyrighted book, or paraphrases of them, lives here only.
+- `labels/`: human labels and blind keys. Tracked, text-free (verdicts and error types, no passage text).
+- `results/`: summaries (numbers only). Tracked.
+
+**Spec.** `docs/experiments/<ID>-<slug>.md` states hypotheses, design, metrics, decision rule, cost, risks. The decision rule is written before any label or result exists and is not changed afterwards; a change is a new version of the spec.
+
+**Provenance.** Each run records the model id, prompt versions and hashes, call and token counts, and the image/commit it ran on, next to its results.
+
+**Copyright.** The book `uiowa-algebra.pdf` and any text derived from it are never committed or released. The public benchmark uses open-licensed books, with hashes and spans only.
+
+**Blindness.** Labels are finished before detector output is opened. Detectors never see labels.
+
+## Related docs
+
+- `docs/research-plan.md`: idea, venue, related work, experiments in full
+- `docs/TODO.md`: task list to 3 Jan 2027
+- `docs/acl-2027-bar.md`: how the paper reaches the venue's bar
+- `docs/infrastructure/runner-lean435.md`: CI runner, Lean/Mathlib environment, images

docs/infrastructure/runner-lean435.md

@@ -0,0 +1,49 @@
+# Runner `ubuntu24.04-x64-lean4.35` (set up 2026-10-21)
+
+Gitea runner `iZ6we8b3jgd6nc2qehu06lZ` (act_runner v5.2.0, runner id 7), label `ubuntu24.04-x64-lean4.35`. Both `lean-bench` and `lean-agent` CI run here; the old `gitea-cicd-server-for-CODEX` label is no longer used.
+
+## The host
+- Jobs run **on the host, not in a container**, as root. Ubuntu 24.04.5, kernel 6.8, 4 CPU, 15 GiB RAM, no swap, 150 GiB system disk (expanded from 100 GiB on 2026-10-28); the ext4 root filesystem reports about 148 GiB, with 75 GiB available immediately after expansion.
+- Lean 4.35.0 via elan 4.2.4 in `/root/.elan`. Python 3.12.3, git 2.43, gcc 13.3, curl, jq.
+- **No Node**, so `actions/checkout` and other JavaScript actions cannot run. Workflows clone with `git fetch --depth 1 origin $SHA` using `${{ github.token }}`.
+- Docker was not installed; the lean-bench `image` job installs `docker.io` + `docker-buildx` (Docker 29.1.3) if missing.
+- Runner capacity appears to be 1: jobs from both repos queue behind each other.
+
+## What CI does
+- **lean-agent** (`.gitea/workflows/ci.yml`): unit tests with the real Lean verifier, a CLI end-to-end run with a scripted provider, and a Mathlib task against lean-bench's host cache (skips if the cache is not ready).
+- **lean-bench** (`.gitea/workflows/ci.yml`): `python` (ruff + pytest) -> `lean` (host Mathlib cache + `docker/smoke.py` with real Lean) -> `image` (build, smoke inside the image, keep). Triggers: push to `main` and `ci/**`, pull requests, manual. `image` is skipped for pull requests.
+- **Image kept on the host**: `lean-bench:latest`, `:main`, `:lean4.35`, `:sha-<short>` (about 15 GB). `latest`/`main` are tagged only from `main`. Nothing prunes old `sha-*` tags.
+- Mathlib host cache: `/opt/lean-cache/leanbench-<hash of lean-toolchain+lakefile>` with a `.ready` marker, created by `.gitea/scripts/prepare-mathlib.sh` under a flock. `import Mathlib` elaborates in about 4 s there.
+
+## Lessons
+- `lake exe cache get` regularly drops a few of about 9,031 files ("Broken pipe" / "Connection reset"), and the same files can fail twice in a row. Retries fix it.
+- Mathlib's post-update hook runs the cache fetch **inside `lake update`**, so retries placed after it never run. Set `MATHLIB_NO_CACHE_ON_UPDATE=1` for `lake update` and fetch in a retry loop. In the image the archives live in a BuildKit cache mount (`/root/.cache/mathlib`), so a retried build resumes.
+- Cold image build about 19 min; with layers cached about 2 min.
+- Gitea 1.26.1 has no cancel-run API; a person cancels in the web UI, then the API can `DELETE` the finished run. The Actions logs endpoint needs a token; the runs/jobs status endpoints work anonymously on this public repo.
+
+## Root capacity expansion (2026-10-28)
+
+The owner expanded the cloud disk to 150 GiB, but root partition `/dev/nvme0n1p3`
+and its ext4 filesystem still occupied about 100 GiB. CI run number 43 (API run ID 438)
+therefore continued to report 28 GiB available and failed its unchanged 30 GiB preflight.
+Rerunning a failed job retains the same UI run number; its job attempt number increments.
+
+Read-only probe run number 45 (API run ID 442) confirmed the raw-disk/partition mismatch.
+Its `growpart -N` output showed that partition 3 could extend from 209301471 to
+314159071 sectors while keeping start sector 413696 and its partition UUID unchanged.
+Temporary files and logs were small; Docker/containerd storage and Mathlib were the main
+consumers. No tagged image, build cache or Mathlib cache was deleted for this repair.
+
+The owner explicitly authorized partition and filesystem expansion in the execution chat.
+Manual maintenance run number 46 (API run ID 443) then backed up the partition table to
+`/root/lean-bench-maintenance/20261028T121919Z/nvme0n1.sfdisk`, expanded partition 3,
+and grew the mounted ext4 filesystem online. The resulting partition is 149.8 GiB;
+`df` reported a 148 GiB filesystem with 75 GiB available. No reboot was required.
+
+`.gitea/workflows/env-probe.yml` now includes read-only storage and cache diagnostics.
+`.gitea/workflows/runner-storage-maintenance.yml` is manual-only and requires the literal
+confirmation `EXPAND_RUNNER_ROOT`. It validates hostname, root device, ext4 type, partition
+UUID, start sector and disk size, takes a lock, and backs up the partition table before any
+change. Future execution still requires explicit owner authorization for that maintenance.
+It never formats a device or prunes images. The failed image job was retried after expansion;
+its actual build, smoke-test and image-retention outcome is recorded in CI run number 43.

experiments/P0-pilot/README.md

@@ -0,0 +1,67 @@
+# P0: pilot
+
+Experiment ID **P0**. Spec, hypotheses, decision rule and costs: `docs/experiments/P0-pilot.md`.
+Registry of all experiments: `docs/experiments/README.md`.
+
+Question: on the 65 existing items, does role alignment (passage simplex vs. Lean simplex) find
+unfaithful formalizations better than a single LLM judge, compile-only, or static lint?
+
+## Layout
+
+    data/      ignored by git: items.jsonl (copy of the 65 items), labelsheet.html, results.jsonl
+               (all contain or paraphrase passages from a copyrighted book)
+    labels/    tracked: key.json (blind id -> item id, no text), labels.json (verdicts and error
+               types only; do not paste passage text into the notes field)
+    results/   tracked: summary.json written by score.py (numbers only)
+
+## Steps
+
+    # Default exports omit source_text. Restore it from the matching private review.
+    python experiments/P0-pilot/prepare_items.py --items runs/p85-110/items.jsonl \
+        --review runs/p85-110/review.json --out experiments/P0-pilot/data/items.jsonl
+    python experiments/P0-pilot/make_sheet.py --items experiments/P0-pilot/data/items.jsonl \
+        --out experiments/P0-pilot/data --key-dir experiments/P0-pilot/labels --seed 7
+    # a person opens data/labelsheet.html, labels all 65 items, downloads labels.json into labels/
+    python experiments/P0-pilot/run_pilot.py --items experiments/P0-pilot/data/items.jsonl \
+        --out experiments/P0-pilot/data/results.jsonl --dry-run
+    python experiments/P0-pilot/run_pilot.py --items experiments/P0-pilot/data/items.jsonl \
+        --out experiments/P0-pilot/data/results.jsonl --labels experiments/P0-pilot/labels/labels.json
+    python experiments/P0-pilot/score.py --results experiments/P0-pilot/data/results.jsonl \
+        --labels experiments/P0-pilot/labels/labels.json --key experiments/P0-pilot/labels/key.json \
+        --summary experiments/P0-pilot/results/summary.json
+
+Labeling must be finished before anyone opens `results.jsonl`.
+
+## Execution safeguards
+
+- Every item must have a nonempty source passage. `prepare_items.py` restores passages only
+  when all exported fields match the archived review; the exported cohort and Lean code stay intact.
+- Freeze all labels before the paid run. The owner changed the labeler to the Codex assistant
+  on 2026-10-28. These are **AI labels, not human gold**; see the metadata in `labels/labels.json`.
+- `--max-calls` counts actual HTTP attempts, including transport and JSON retries, cumulatively
+  across resumes. The hard ceiling is 400. A reservation is saved before each request; an interrupted
+  request may consume a reservation without a known response or token count.
+- Metadata is stored beside the output as `results.meta.json`. Model, endpoint, temperature,
+  input hash, frozen-label hash and prompt hashes must match on resume. Usage is cumulative.
+  A file lock prevents concurrent writers. A budget stop returns exit status 2.
+- The nominal successful path uses 130 calls (one source extraction and one judge per item);
+  malformed replies and network retries may increase the actual count.
+- Scoring requires complete labels and results and no unresolved detector errors. The primary
+  comparison is wrong versus faithful; minor drift is included as positive in the secondary analysis.
+  The complementary-signal PARTIAL rule counts wrong items flagged by role alignment but missed
+  by the judge. No threshold, concept table or detector prompt was tuned for these labels.
+- Raw passages, labeling HTML and model responses remain in the ignored `data/` directory.
+  Only verdicts, abstract annotation notes, hashes and text-free summaries belong in Git.
+
+## Separate GPT-assisted diagnostic
+
+The owner requested a complete 65-item reassessment by the current GPT assistant on
+2026-10-28. This is separate from the incomplete Qwen run: no outputs are mixed and
+neither the earlier labels nor Qwen files are overwritten. The assistant had prior
+exposure to the reference labels and Lean; this is not blind or independent validation.
+No GO/PARTIAL/NO-GO decision is issued.
+
+See `docs/experiments/P0-gpt-diagnostic.md` for all counts, limitations, artifact locations
+and the offline replay command. The tracked `results/gpt-diagnostic-*.json` files contain
+only categorical/numeric outputs and audit metadata. The authored source structures,
+reasons and full review page stay in the ignored `data/gpt-diagnostic/` directory.

experiments/P0-pilot/assistant_diagnostic.py

@@ -0,0 +1,200 @@
+"""Validate and replay a current-chat assistant review without calling any model.
+
+Private source schemas and reasons stay in data/. Public summaries contain only
+categories, counts, numeric scores, hashes and an explicit non-independent provenance.
+"""
+from __future__ import annotations
+
+import argparse
+import hashlib
+import html
+import json
+import math
+from collections import Counter
+from pathlib import Path
+
+from leanbench.align import DEFAULT_THRESHOLD, GOAL_THRESHOLD, align
+from leanbench.evalstats import auc, confusion, wilson
+from leanbench.lint import lint
+from leanbench.project import project
+from leanbench.srcsimplex import parse_source_simplex
+
+VERDICTS = {"faithful", "minor_drift", "wrong", "not_formalizable"}
+ERRORS = {"missing_hypothesis", "extra_hypothesis", "wrong_type", "quantifier",
+          "wrong_conclusion", "degenerate", "hallucinated_api", "other"}
+
+
+def digest(path: Path) -> str:
+    return hashlib.sha256(path.read_bytes()).hexdigest()
+
+
+def finite(value):
+    if isinstance(value, dict):
+        return {k: finite(v) for k, v in value.items()}
+    if isinstance(value, (list, tuple)):
+        return [finite(v) for v in value]
+    if isinstance(value, float) and not math.isfinite(value):
+        return None
+    return value
+
+
+def unique(rows, field):
+    indexed = {row[field]: row for row in rows}
+    if len(indexed) != len(rows):
+        raise ValueError(f"Duplicate {field}")
+    return indexed
+
+
+def evaluate(items, key, assessment):
+    """Keep model-authored assessments separate from deterministic detector outputs."""
+    by_id = unique(items, "id")
+    records = unique(assessment["records"], "blind_id")
+    if (not key or len(set(key.values())) != len(key) or set(records) != set(key)
+            or set(by_id) != set(key.values())):
+        raise ValueError("Items, key and assessments must cover the same cohort exactly once")
+    output = []
+    for blind, item_id in key.items():
+        item, record = by_id[item_id], records[blind]
+        if record["id"] != item_id or not item.get("source_text", "").strip():
+            raise ValueError(f"Missing source text or mismatched item for {blind}")
+        judge = record["judge"]
+        if (judge.get("verdict") not in VERDICTS or type(judge.get("faithful")) is not bool
+                or judge["faithful"] != (judge["verdict"] == "faithful")
+                or not isinstance(judge.get("reason"), str) or not judge["reason"].strip()
+                or not isinstance(judge.get("errors"), list)
+                or not set(judge["errors"]) <= ERRORS):
+            raise ValueError(f"Invalid authored judgment for {blind}")
+        source = parse_source_simplex(record["source"])
+        projection = project(item["lean_code"])
+        alignment = align(source, projection)
+        output.append({"id": item_id, "blind_id": blind,
+                       "source": source.as_dict(), "judge": judge,
+                       "projection": projection.as_dict(), "role": alignment.as_dict(),
+                       "lint": lint(projection), "compiled": bool(item.get("verified")),
+                       "errors": {}})
+    return output
+
+
+def public_items(rows, labels):
+    if set(labels) != {row["blind_id"] for row in rows}:
+        raise ValueError("Reference labels must cover the entire cohort")
+    out = []
+    for row in rows:
+        reference = labels[row["blind_id"]]["verdict"]
+        if reference not in VERDICTS:
+            raise ValueError("Invalid reference verdict")
+        out.append({"blind_id": row["blind_id"], "reference_verdict": reference,
+                    "assistant_verdict": row["judge"]["verdict"],
+                    "assistant_error_types": row["judge"]["errors"],
+                    "verdict_agrees": reference == row["judge"]["verdict"],
+                    "compiled": row["compiled"], "lint_flagged": bool(row["lint"]),
+                    "role_flagged": row["role"]["flagged"],
+                    "role_score": row["role"]["score"],
+                    "role_conflict_types": row["role"]["errors"],
+                    "source_role_count": len(row["source"]["roles"]),
+                    "lean_role_count": len(row["projection"]["roles"]),
+                    "degenerate_projection": row["projection"]["degenerate"]})
+    return out
+
+
+def agreement(rows, labels, secondary=False):
+    cohort = [r for r in rows if labels[r["blind_id"]]["verdict"] != "not_formalizable"
+              and (secondary or labels[r["blind_id"]]["verdict"] != "minor_drift")]
+    positives = {"wrong", "minor_drift"} if secondary else {"wrong"}
+    target = [labels[r["blind_id"]]["verdict"] in positives for r in cohort]
+    out = {}
+    for name, flags in {
+        "role": [r["role"]["flagged"] for r in cohort],
+        "assistant_judge": [not r["judge"]["faithful"] for r in cohort],
+        "lint": [bool(r["lint"]) for r in cohort],
+        "compile_only": [not r["compiled"] for r in cohort],
+    }.items():
+        counts = confusion(flags, target)
+        out[name] = {**counts.as_dict(), "precision_ci": wilson(counts.tp, counts.tp + counts.fp)}
+    out["role"]["auc"] = auc([-r["role"]["score"] for r in cohort], target)
+    return {"n": len(cohort), "metrics_are_non_independent_reference_agreement": True,
+            "detectors": out}
+
+
+def write_review(path, rows, items):
+    by_id = {r["id"]: r for r in items}
+    sections = []
+    for row in rows:
+        item = by_id[row["id"]]
+        sections.append(
+            f'<section id="{html.escape(row["blind_id"])}"><h2>{row["blind_id"]}</h2>'
+            f'<h3>Passage</h3><pre>{html.escape(item["source_text"])}</pre>'
+            f'<h3>Lean</h3><pre>{html.escape(item["lean_code"])}</pre>'
+            f'<h3>Fresh assistant judgment: {row["judge"]["verdict"]}</h3>'
+            f'<p>{html.escape(row["judge"]["reason"])}</p>'
+            f'<h3>Source roles</h3><pre>{html.escape(json.dumps(row["source"], indent=2, ensure_ascii=False))}</pre>'
+            f'<h3>Deterministic alignment</h3><pre>{html.escape(json.dumps(row["role"], indent=2, ensure_ascii=False))}</pre></section>'
+        )
+    path.write_text('<!doctype html><html lang="en"><meta charset="utf-8">'
+                    '<title>P0 GPT-assisted diagnostic</title><style>'
+                    'body{font:16px/1.6 system-ui;max-width:1050px;margin:32px auto;padding:0 20px}'
+                    'pre{white-space:pre-wrap;overflow-wrap:anywhere;background:#f4f5f6;padding:16px}'
+                    'section{border-top:1px solid #ccc;margin:40px 0}</style>'
+                    '<h1>P0: 65-item GPT-assisted diagnostic</h1>'
+                    '<p>Private review. Same-assistant, non-blind diagnosis; no independent accuracy or gate decision. '
+                    'Passages and model-derived descriptions must remain outside Git.</p>'
+                    + ''.join(sections) + '</html>', encoding="utf-8")
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--items", type=Path, required=True)
+    parser.add_argument("--key", type=Path, required=True)
+    parser.add_argument("--assessments", type=Path, required=True)
+    parser.add_argument("--labels", type=Path, required=True)
+    parser.add_argument("--private-out", type=Path, required=True)
+    parser.add_argument("--summary", type=Path, required=True)
+    parser.add_argument("--public-items", type=Path, required=True)
+    args = parser.parse_args()
+    if "data" not in args.private_out.parts:
+        parser.error("Private output must be under the gitignored data/ directory")
+    items = [json.loads(x) for x in args.items.read_text().splitlines() if x.strip()]
+    key = json.loads(args.key.read_text())["key"]
+    assessment = json.loads(args.assessments.read_text())
+    provenance = assessment["provenance"]
+    if (provenance["items_sha256"] != digest(args.items)
+            or provenance["key_sha256"] != digest(args.key)):
+        parser.error("Authored review is bound to different inputs or blind key")
+    rows = evaluate(items, key, assessment)
+    labels = json.loads(args.labels.read_text())["labels"]
+    public = public_items(rows, labels)
+    summary = {
+        "experiment": "P0-GPT-diagnostic", "status": "complete", "n": len(rows),
+        "provenance": provenance, "decision": None,
+        "decision_withheld_reason": "Same-assistant, non-blind diagnostic; not the preregistered Qwen pilot or independent ground-truth validation.",
+        "hashes": {"items": digest(args.items), "key": digest(args.key),
+                   "assessments": digest(args.assessments), "reference_labels": digest(args.labels),
+                   "replay_script": digest(Path(__file__)),
+                   **{f"leanbench/{name}.py": digest(Path(__file__).resolve().parents[2] / "leanbench" / f"{name}.py")
+                      for name in ("align", "project", "srcsimplex", "lint")}},
+        "fixed_thresholds": {"matching": DEFAULT_THRESHOLD, "goal": GOAL_THRESHOLD},
+        "verdict_counts": dict(Counter(r["judge"]["verdict"] for r in rows)),
+        "role_flagged": sum(r["role"]["flagged"] for r in rows),
+        "lint_flagged": sum(bool(r["lint"]) for r in rows),
+        "compiled": sum(r["compiled"] for r in rows),
+        "degenerate_projection": sum(r["projection"]["degenerate"] for r in rows),
+        "exact_verdict_agreement": sum(r["verdict_agrees"] for r in public),
+        "changed_verdicts": [r["blind_id"] for r in public if not r["verdict_agrees"]],
+        "primary_reference_agreement": agreement(rows, labels),
+        "secondary_reference_agreement": agreement(rows, labels, secondary=True),
+        "role_flagged_by_new_verdict": {v: {"n": sum(r["judge"]["verdict"] == v for r in rows),
+             "flagged": sum(r["judge"]["verdict"] == v and r["role"]["flagged"] for r in rows)}
+             for v in sorted(VERDICTS)},
+    }
+    args.private_out.mkdir(parents=True, exist_ok=True)
+    (args.private_out / "results.jsonl").write_text(''.join(json.dumps(r, ensure_ascii=False) + '\n' for r in rows))
+    write_review(args.private_out / "review.html", rows, items)
+    args.summary.parent.mkdir(parents=True, exist_ok=True)
+    args.public_items.parent.mkdir(parents=True, exist_ok=True)
+    args.summary.write_text(json.dumps(finite(summary), indent=2, allow_nan=False) + '\n')
+    args.public_items.write_text(json.dumps(public, indent=2, allow_nan=False) + '\n')
+    print(json.dumps({k: summary[k] for k in ("n", "status", "verdict_counts", "role_flagged", "exact_verdict_agreement", "decision")}))
+
+
+if __name__ == "__main__":
+    main()

experiments/P0-pilot/labels/key.json

@@ -0,0 +1,71 @@
+{
+  "seed": 7,
+  "items_file": "items.jsonl",
+  "key": {
+    "P01": "548ab1a767a685aefa146455",
+    "P02": "6ea85a17cb5decb0670c4afe",
+    "P03": "389a27cbae1957943fae2960",
+    "P04": "b63f0ed4d1ea1e11e34e6f8a",
+    "P05": "db4553333550bccbd3f0e21d",
+    "P06": "c3e75089fbfe8f386b4a22ec",
+    "P07": "91a6a0c1c21014bf08ffa3b6",
+    "P08": "675ac9dbf3ec8a0553149a96",
+    "P09": "8b39fc5b656bac00bc1e863f",
+    "P10": "3549ad65eee67f7b432a8b70",
+    "P11": "0b7db1a8100c33a50a08981f",
+    "P12": "e3d40d93cda13ec59c35d9a5",
+    "P13": "aaf1250a5104a4f7c1ca0d29",
+    "P14": "57966f39253aba58777a4ffd",
+    "P15": "6ef921c49672c73f8f3e0edf",
+    "P16": "371fe1b32fe04da354ad4478",
+    "P17": "a7396b1a5d5ebcd5b48ea7ba",
+    "P18": "59bb865c9bdfb8521e414743",
+    "P19": "283d407566264b02fbee6560",
+    "P20": "7de228e675b949cd64850c04",
+    "P21": "dc1c450987f3e3a5285260f7",
+    "P22": "c42dc687ecc042f5b7a00a9d",
+    "P23": "8491370b02906b6efdb3da5e",
+    "P24": "437d02fe69d580bde075648c",
+    "P25": "5fe4f3fbbead7e6988f015a9",
+    "P26": "8a55f59982e50e4af47b3d55",
+    "P27": "8d4d64143a8b214e38d7ba1b",
+    "P28": "6017927fdafd91ca22ed6ade",
+    "P29": "089c452ec2f9b850733a44f6",
+    "P30": "75009c3d616f02be4d7a5824",
+    "P31": "9091f6a277215174e821d373",
+    "P32": "0cd2f0368a0d8234c2593845",
+    "P33": "8e55e625fa9b10b7b65f59f4",
+    "P34": "534c6ffcf56931559e70657b",
+    "P35": "aa16561dceee591e35e42c4d",
+    "P36": "73ec95bfac2896218d2b1dab",
+    "P37": "6b5a55ec3bb3c85239919649",
+    "P38": "d6ddc1df3ce6b764f3fb8d73",
+    "P39": "ed87589326312890bea42d7c",
+    "P40": "d609c5bb746fc0e05625134a",
+    "P41": "4405f31187373d5e1de622d2",
+    "P42": "05a6defa23576b7da41f8fbf",
+    "P43": "47c39e88c29e3974e8864e90",
+    "P44": "fa61f8cb0e88b11e158c4eec",
+    "P45": "3c00c37b39285cbd7d0be732",
+    "P46": "186d922a4121917ac8643316",
+    "P47": "e845a95d7b5054a0dbdf34eb",
+    "P48": "e7a3cec23c2ecdc655dd12cf",
+    "P49": "e966f3b17e32318acd5f2762",
+    "P50": "2c420bf6ec32069ecd0043dc",
+    "P51": "25af34567cb2040bf41869e5",
+    "P52": "578ae89f353ecbdc0ffb76a2",
+    "P53": "1a8d6a5c9aa3cc5000dee474",
+    "P54": "450c7df89ecd284b0e08504a",
+    "P55": "f908ac15b1bf8228281bcf68",
+    "P56": "bcdfa01447e7060e1fd3d935",
+    "P57": "f86421f93f1381d2ce728bc1",
+    "P58": "89fe687db9136379cd276fff",
+    "P59": "da65aa56505f6c13e6553d0d",
+    "P60": "ab2990e9786d5bda5a04e067",
+    "P61": "a892779bfcaca35b91e7d611",
+    "P62": "7593062cab7c74cdecec08d0",
+    "P63": "c8204e9d19a6dd5d730dccc7",
+    "P64": "b40279b634fffd0841ff0f5a",
+    "P65": "f8d2e206681972927560be2c"
+  }
+}

experiments/P0-pilot/labels/labels.json

@@ -0,0 +1,427 @@
+{
+  "labeler": "Codex AI assistant (this chat; exact deployed model identifier unavailable)",
+  "labeler_type": "AI; not human gold",
+  "frozen_at": "2026-10-28T10:42:10.032234+00:00",
+  "items_sha256": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed",
+  "key_sha256": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836",
+  "method": "Single-pass semantic annotation in shuffled blind-ID order; per-item compiler outcomes and detector outputs hidden. Pure syntax/proof defects are ignored when meaning is recoverable. No compiler/API-name audit. Full extracted-span coverage is assessed; unspecified design tasks or unresolved contextual references are not formalizable.",
+  "limitations": [
+    "Single AI annotator; no human adjudication or inter-annotator agreement.",
+    "The annotator reviewed detector implementation and aggregate compilation counts before labeling; only per-item outputs were hidden.",
+    "AI labels replace the originally planned human/Kimi labels by explicit owner instruction in this chat; the original human-ground-truth protocol is therefore not fully satisfied."
+  ],
+  "labels": {
+    "P01": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The field axioms and nontriviality match the stated definition."
+    },
+    "P02": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The whole carrier and identity singleton are the two specified subgroups; API spelling is not assessed."
+    },
+    "P03": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Every integer unit is constrained to the two specified values."
+    },
+    "P04": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Generated subgroup is equated with all integer powers; escaped notation is treated as a syntax defect."
+    },
+    "P05": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Existence of a bijective multiplication-preserving map matches the definition."
+    },
+    "P06": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The theorem statement gives exactly the inverse-of-product identity; proof validity is not assessed."
+    },
+    "P07": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "Only already-assumed prime factors are asserted to exist; no recovery from the totient is specified."
+    },
+    "P08": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Both identity preservation and inverse preservation are stated under a multiplicative equivalence."
+    },
+    "P09": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "The multiplicative ring carrier does not encode the additive cyclic group, and the second extracted exercise is omitted."
+    },
+    "P10": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Both left and right equations have unique solutions."
+    },
+    "P11": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The group cardinality is the exponent, with the correct identity and quantification."
+    },
+    "P12": {
+      "verdict": "not_formalizable",
+      "errors": [
+        "other"
+      ],
+      "notes": "The extracted design question provides no formal security or authentication specification for a fidelity comparison."
+    },
+    "P13": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "The intended modular identity is retained, but the integer variable is supplied to a natural-number coprimality predicate."
+    },
+    "P14": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "Only existence of a ring structure is stated; the identity and unit characterization are omitted."
+    },
+    "P15": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Unique solvability in both factors expresses the row and column permutation property."
+    },
+    "P16": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Passing to the product representation preserves the order-divisibility claim; capitalization and namespace errors are not semantic changes."
+    },
+    "P17": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "An independent non-field example in the extracted passage is omitted."
+    },
+    "P18": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The norm-one complex carrier and multiplication describe the specified subgroup; bundling/API validity is not assessed."
+    },
+    "P19": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "The natural-valued order convention needs an infinite-order convention absent from the cardinality definition."
+    },
+    "P20": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "A single left-identity action on one group element forces equality to the identity."
+    },
+    "P21": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "The intended commutativity equivalence is visible, but the left operation lacks the carrier annotation needed to identify G."
+    },
+    "P22": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The two quantified unique-solvability claims express the specified table property."
+    },
+    "P23": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Prime factors, modulus, lcm exponent and coprimality reproduce the extracted claim; no unstated distinctness assumption is introduced."
+    },
+    "P24": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "An arbitrary group satisfying an order condition is not identified with the geometric symmetry group."
+    },
+    "P25": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The two declarations cover both cancellation directions."
+    },
+    "P26": {
+      "verdict": "wrong",
+      "errors": [
+        "extra_hypothesis",
+        "missing_hypothesis"
+      ],
+      "notes": "The inserted divisibility assumption does not express the RSA relationship required by the argument."
+    },
+    "P27": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "The isomorphism is asserted for a quotient of the ambient group instead of the stabilizer subgroup."
+    },
+    "P28": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "Natural exponent division fails to express a square root, and the homomorphism target does not encode the specified automorphism."
+    },
+    "P29": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "A bijective homomorphism supplies the isomorphism assumption and both power assertions are retained."
+    },
+    "P30": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "An unordered finite product is used for an arbitrary semigroup, losing the ordered nonempty product required by the exercise."
+    },
+    "P31": {
+      "verdict": "not_formalizable",
+      "errors": [
+        "other"
+      ],
+      "notes": "The isolated instruction refers to an earlier map whose definition is absent; the actual proposition cannot be recovered from this span."
+    },
+    "P32": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "The result merely supplies an unspecified ring homomorphism and does not constrain it to evaluation at the matrix parameter."
+    },
+    "P33": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The cardinality assumption and the nonidentity involution conclusion match; the missing instance binder is a compilation defect."
+    },
+    "P34": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The contrasting abelian properties encode the reason these specified groups are not isomorphic."
+    },
+    "P35": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "quantifier"
+      ],
+      "notes": "One fixed-arity function is applied at incompatible arities instead of specifying a coherent family of products."
+    },
+    "P36": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "The ring carrier replaces the concrete root-of-unity group, and neither its order nor the specified generator is stated."
+    },
+    "P37": {
+      "verdict": "wrong",
+      "errors": [
+        "degenerate",
+        "wrong_conclusion"
+      ],
+      "notes": "The declaration has no defining expression for the requested subgroup."
+    },
+    "P38": {
+      "verdict": "wrong",
+      "errors": [
+        "missing_hypothesis"
+      ],
+      "notes": "Nonemptiness is missing, so the empty subset satisfies both closure assumptions."
+    },
+    "P39": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "Laurent series replace finite Laurent polynomials, and the requested units are not characterized."
+    },
+    "P40": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The supplied structure body fixes the function to the canonical integer residue map."
+    },
+    "P41": {
+      "verdict": "wrong",
+      "errors": [
+        "extra_hypothesis"
+      ],
+      "notes": "The cardinality assertion is restricted to the range where noncommutativity holds, dropping the smaller symmetric groups."
+    },
+    "P42": {
+      "verdict": "wrong",
+      "errors": [
+        "missing_hypothesis",
+        "wrong_conclusion"
+      ],
+      "notes": "A necessary closure condition is promoted to sufficiency without inverse closure."
+    },
+    "P43": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Any two groups of the specified size are related by a multiplicative equivalence."
+    },
+    "P44": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The defining field is exactly commutativity of the group operation."
+    },
+    "P45": {
+      "verdict": "wrong",
+      "errors": [
+        "quantifier",
+        "wrong_conclusion"
+      ],
+      "notes": "Literal uniqueness of a carrier/structure replaces uniqueness up to group isomorphism."
+    },
+    "P46": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "wrong_conclusion"
+      ],
+      "notes": "Univariate polynomials over a product ring replace three-variable real polynomials; the units question is omitted."
+    },
+    "P47": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "The integer-span equality captures the generated set, but the equality for opposite generators is not explicitly stated."
+    },
+    "P48": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The one-sided inverse hypothesis gives the specified inverse element."
+    },
+    "P49": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The theorem statement is exactly involutivity of group inversion."
+    },
+    "P50": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The custom structure supplies additive commutative group, associative multiplication and both distributive laws without imposing a unit."
+    },
+    "P51": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The carrier, multiplication and identity encode the specified finite group; existence of the chosen API is not audited."
+    },
+    "P52": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "Ring structure and unit-to-constant direction are present, but identity characterization is replaced by reflexivity."
+    },
+    "P53": {
+      "verdict": "minor_drift",
+      "errors": [
+        "extra_hypothesis"
+      ],
+      "notes": "Cardinality is represented only for finite groups although the definition is not restricted to them."
+    },
+    "P54": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "Multiplicative subgroup closure of a residue is used in place of the additive cyclic subgroup generated by it."
+    },
+    "P55": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The abelian-property equivalence is stated under an isomorphism."
+    },
+    "P56": {
+      "verdict": "not_formalizable",
+      "errors": [
+        "other"
+      ],
+      "notes": "The design question does not specify an authenticity predicate or formal adversarial model."
+    },
+    "P57": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion"
+      ],
+      "notes": "The homomorphism criterion is retained but the separate isomorphism definition is absent."
+    },
+    "P58": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "A multiplicative equivalence on the full residue ring does not represent the additive cyclic group in the comparison."
+    },
+    "P59": {
+      "verdict": "minor_drift",
+      "errors": [
+        "wrong_type"
+      ],
+      "notes": "The inherited-group criterion is recognizable, but operations on the subset are not specified as restricted operations."
+    },
+    "P60": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_type",
+        "missing_hypothesis"
+      ],
+      "notes": "Global bijections with local differentiability conditions do not specify self-diffeomorphisms of the open subset."
+    },
+    "P61": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "The homeomorphism type supplies the intended carrier and group structure under composition; notation validity is not assessed."
+    },
+    "P62": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Both least-positive exponent and the bounded-power description are retained, ignoring set-minimum API syntax."
+    },
+    "P63": {
+      "verdict": "faithful",
+      "errors": [],
+      "notes": "Both two-sided identity hypotheses and their equality are stated."
+    },
+    "P64": {
+      "verdict": "wrong",
+      "errors": [
+        "missing_hypothesis",
+        "extra_hypothesis"
+      ],
+      "notes": "The exponent relation uses the ciphertext modulus where the RSA exponent modulus is required."
+    },
+    "P65": {
+      "verdict": "wrong",
+      "errors": [
+        "wrong_conclusion",
+        "degenerate"
+      ],
+      "notes": "The arbitrary finite group is unrelated to the requested geometric symmetries, with the classification left in a comment."
+    }
+  }
+}

experiments/P0-pilot/make_sheet.py

@@ -1,13 +1,14 @@
 """Build the blind labeling sheet for the pilot.
 
-    python experiments/pilot/make_sheet.py --items runs/p85-110/items.jsonl \
-        --out runs/pilot/private --seed 7
+    python experiments/P0-pilot/make_sheet.py --items experiments/P0-pilot/data/items.jsonl \
+        --out experiments/P0-pilot/data --key-dir experiments/P0-pilot/labels --seed 7
 
-Writes, into a directory that must stay local (it contains passages from a
-copyrighted book; ``runs/`` and ``**/private/`` are gitignored):
+Writes:
 
-    labelsheet.html     open in a browser; label every item; press "Download labels.json"
-    key.json            blind id -> item id (keep it; the scorer needs it)
+    <out>/labelsheet.html    open in a browser; label every item; press "Download labels.json".
+                             Contains passages from a copyrighted book, so ``data/`` is gitignored.
+    <key-dir>/key.json       blind id -> item id. Text-free, so it is tracked in git; save the
+                             downloaded labels.json next to it.
 
 The sheet shows the passage and the Lean code. It deliberately hides whether Lean
 accepted the code, any model output, and any score, so the labels are independent of
@@ -146,12 +147,17 @@ def card(blind: str, item: dict) -> str:
 def main() -> int:
     parser = argparse.ArgumentParser(description=__doc__.splitlines()[0])
     parser.add_argument("--items", required=True, type=Path)
-    parser.add_argument("--out", required=True, type=Path)
+    parser.add_argument("--out", required=True, type=Path, help="where labelsheet.html goes (ignored by git)")
+    parser.add_argument("--key-dir", type=Path, default=None, help="where key.json goes (default: ../labels)")
     parser.add_argument("--seed", type=int, default=7)
     args = parser.parse_args()
 
     items = [json.loads(line) for line in args.items.read_text(encoding="utf-8").splitlines()
              if line.strip()]
+    if not items or any(not item.get("source_text", "").strip() for item in items):
+        parser.error("Every item needs nonempty source_text; use a private source-inclusive export.")
+    if len({item["id"] for item in items}) != len(items):
+        parser.error("Item IDs must be unique.")
     order = list(range(len(items)))
     random.Random(args.seed).shuffle(order)
     blind_ids = [f"P{n:02d}" for n in range(1, len(items) + 1)]
@@ -159,16 +165,18 @@ def main() -> int:
 
     legend = "".join(f"<li><b>{esc(n)}</b>: {esc(d)}</li>" for _, n, d in FIDELITY)
     cards = "\n".join(card(blind_ids[pos], items[idx]) for pos, idx in enumerate(order))
+    key_dir = args.key_dir or args.out.parent / "labels"
     args.out.mkdir(parents=True, exist_ok=True)
+    key_dir.mkdir(parents=True, exist_ok=True)
     (args.out / "labelsheet.html").write_text(
         PAGE.format(n=len(items), legend=legend, cards=cards, ids=json.dumps(blind_ids)),
         encoding="utf-8",
     )
-    (args.out / "key.json").write_text(
+    (key_dir / "key.json").write_text(
         json.dumps({"seed": args.seed, "items_file": args.items.name, "key": key}, indent=2),
         encoding="utf-8",
     )
-    print(f"wrote {args.out/'labelsheet.html'} ({len(items)} items) and key.json")
+    print(f"wrote {args.out/'labelsheet.html'} ({len(items)} items) and {key_dir/'key.json'}")
     return 0
 
 

experiments/P0-pilot/prepare_items.py

@@ -0,0 +1,45 @@
+"""Restore source passages from a private archived review without changing the cohort."""
+from __future__ import annotations
+
+import argparse
+import json
+from pathlib import Path
+
+
+def restore(items: list[dict], review: dict) -> list[dict]:
+    archived = review["items"]
+    by_id = {row["id"]: row for row in archived}
+    if len(by_id) != len(archived) or len({row["id"] for row in items}) != len(items):
+        raise ValueError("Duplicate item IDs")
+    restored = []
+    for item in items:
+        original = by_id[item["id"]]
+        comparable = dict(original)
+        if isinstance(comparable.get("imports"), str):
+            comparable["imports"] = json.loads(comparable["imports"])
+        if any(comparable.get(k) != v for k, v in item.items()):
+            raise ValueError(f"Archived review does not match item {item['id']}")
+        passage = original.get("source_text", "")
+        if not passage.strip():
+            raise ValueError(f"Missing archived passage for {item['id']}")
+        restored.append({**item, "source_text": passage})
+    return restored
+
+
+def main() -> None:
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--items", required=True, type=Path)
+    parser.add_argument("--review", required=True, type=Path)
+    parser.add_argument("--out", required=True, type=Path)
+    args = parser.parse_args()
+    if args.out.parent.name != "data":
+        parser.error("Source-inclusive output must go in a gitignored data/ directory")
+    items = [json.loads(line) for line in args.items.read_text().splitlines() if line.strip()]
+    rows = restore(items, json.loads(args.review.read_text()))
+    args.out.parent.mkdir(parents=True, exist_ok=True)
+    args.out.write_text("".join(json.dumps(row, ensure_ascii=False) + "\n" for row in rows))
+    print(f"Restored {len(rows)} passages; all exported fields are unchanged")
+
+
+if __name__ == "__main__":
+    main()

experiments/P0-pilot/results/gpt-diagnostic-summary.json

@@ -0,0 +1,275 @@
+{
+  "experiment": "P0-GPT-diagnostic",
+  "status": "complete",
+  "n": 65,
+  "provenance": {
+    "run_kind": "current-chat assistant-authored diagnostic; not an API benchmark",
+    "evaluator": "Codex GPT assistant; exact deployed model identifier unavailable",
+    "authored_at": "2026-10-28T11:23:06.275167+00:00",
+    "items_sha256": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed",
+    "key_sha256": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836",
+    "reference_labels_seen_in_prior_chat": true,
+    "lean_seen_while_authoring_source_roles": true,
+    "new_external_api_calls": 0,
+    "assistant_token_usage": null,
+    "limitations": [
+      "Same assistant previously authored the reference labels; agreement is not independent accuracy.",
+      "Prior context contains the earlier review and detector code. This is not a blinded source-only extraction or a fresh-model replicate.",
+      "All judgments are manually authored in this chat, not responses from a GPT API endpoint.",
+      "Semantics are assessed conditionally on recoverable notation. No new Lean compilation or library API audit is performed.",
+      "The strict Boolean judge flags all verdicts except faithful, including not_formalizable; four-way verdicts are also retained."
+    ]
+  },
+  "decision": null,
+  "decision_withheld_reason": "Same-assistant, non-blind diagnostic; not the preregistered Qwen pilot or independent ground-truth validation.",
+  "hashes": {
+    "items": "487ecd22919a5e3b0174a2846ab8fe7c0daf4d3feccccf8ea6571aec04c41bed",
+    "key": "f827cac92ee4e907554fadcc7c0e006ef2b829350f74e7f8b54ca11945e62836",
+    "assessments": "f12735802ba0d4d94b776a91581a13a508eab0ce90ba8973a6c9c4e4d1390272",
+    "reference_labels": "1552dba85e75426799151384e7e28c9a0b1072ed4c862df0876df89920d2a638",
+    "replay_script": "5c02e3d26761ce0b4e38d4be9e65b95bfd8db048c9c7c73edaac17e654e10c0f",
+    "leanbench/align.py": "730e44f1158e6e441e4745dff7324e565b89b6e5148017c3fd93f4c69c22c9ce",
+    "leanbench/project.py": "8ed76924b463ba418ceb732d0fcb6c572a548d94fe7f23759c67746da24d9430",
+    "leanbench/srcsimplex.py": "d10b785299ceb17cadc4e97737eef74183ed390d04b4571a702cd4fd42b069d0",
+    "leanbench/lint.py": "4396e879312f370cd70beeffcbd7ffeab8a41ee1704cc1f235dbbcd6e843fd68"
+  },
+  "fixed_thresholds": {
+    "matching": 0.3,
+    "goal": 0.2
+  },
+  "verdict_counts": {
+    "faithful": 25,
+    "minor_drift": 13,
+    "wrong": 24,
+    "not_formalizable": 3
+  },
+  "role_flagged": 55,
+  "lint_flagged": 21,
+  "compiled": 10,
+  "degenerate_projection": 15,
+  "exact_verdict_agreement": 59,
+  "changed_verdicts": [
+    "P02",
+    "P18",
+    "P23",
+    "P34",
+    "P51",
+    "P57"
+  ],
+  "primary_reference_agreement": {
+    "n": 55,
+    "metrics_are_non_independent_reference_agreement": true,
+    "detectors": {
+      "role": {
+        "tp": 25,
+        "fp": 21,
+        "fn": 0,
+        "tn": 9,
+        "n": 55,
+        "recall": 1.0,
+        "precision": 0.5434782608695652,
+        "false_flag_rate": 0.7,
+        "f1": 0.704225352112676,
+        "recall_ci": [
+          0.8668035060468213,
+          1.0
+        ],
+        "false_flag_ci": [
+          0.5212387898833981,
+          0.8333543735604105
+        ],
+        "precision_ci": [
+          0.4017993496608042,
+          0.67845489578878
+        ],
+        "auc": 0.61
+      },
+      "assistant_judge": {
+        "tp": 25,
+        "fp": 5,
+        "fn": 0,
+        "tn": 25,
+        "n": 55,
+        "recall": 1.0,
+        "precision": 0.8333333333333334,
+        "false_flag_rate": 0.16666666666666666,
+        "f1": 0.9090909090909091,
+        "recall_ci": [
+          0.8668035060468213,
+          1.0
+        ],
+        "false_flag_ci": [
+          0.07336434240351683,
+          0.33564705185680177
+        ],
+        "precision_ci": [
+          0.6643529481431982,
+          0.9266356575964831
+        ]
+      },
+      "lint": {
+        "tp": 12,
+        "fp": 5,
+        "fn": 13,
+        "tn": 25,
+        "n": 55,
+        "recall": 0.48,
+        "precision": 0.7058823529411765,
+        "false_flag_rate": 0.16666666666666666,
+        "f1": 0.5714285714285713,
+        "recall_ci": [
+          0.30031003928960015,
+          0.6650178204685269
+        ],
+        "false_flag_ci": [
+          0.07336434240351683,
+          0.33564705185680177
+        ],
+        "precision_ci": [
+          0.468664666737861,
+          0.8672020613444361
+        ]
+      },
+      "compile_only": {
+        "tp": 24,
+        "fp": 24,
+        "fn": 1,
+        "tn": 6,
+        "n": 55,
+        "recall": 0.96,
+        "precision": 0.5,
+        "false_flag_rate": 0.8,
+        "f1": 0.6575342465753424,
+        "recall_ci": [
+          0.8045552759497747,
+          0.9929039496133008
+        ],
+        "false_flag_ci": [
+          0.6269395261897256,
+          0.9049502189759876
+        ],
+        "precision_ci": [
+          0.36389098932037767,
+          0.6361090106796223
+        ]
+      }
+    }
+  },
+  "secondary_reference_agreement": {
+    "n": 62,
+    "metrics_are_non_independent_reference_agreement": true,
+    "detectors": {
+      "role": {
+        "tp": 32,
+        "fp": 21,
+        "fn": 0,
+        "tn": 9,
+        "n": 62,
+        "recall": 1.0,
+        "precision": 0.6037735849056604,
+        "false_flag_rate": 0.7,
+        "f1": 0.7529411764705882,
+        "recall_ci": [
+          0.8928172849426366,
+          1.0
+        ],
+        "false_flag_ci": [
+          0.5212387898833981,
+          0.8333543735604105
+        ],
+        "precision_ci": [
+          0.4694123578888073,
+          0.7241078808096105
+        ],
+        "auc": 0.590625
+      },
+      "assistant_judge": {
+        "tp": 32,
+        "fp": 5,
+        "fn": 0,
+        "tn": 25,
+        "n": 62,
+        "recall": 1.0,
+        "precision": 0.8648648648648649,
+        "false_flag_rate": 0.16666666666666666,
+        "f1": 0.927536231884058,
+        "recall_ci": [
+          0.8928172849426366,
+          1.0
+        ],
+        "false_flag_ci": [
+          0.07336434240351683,
+          0.33564705185680177
+        ],
+        "precision_ci": [
+          0.7202227252929444,
+          0.9408679273749238
+        ]
+      },
+      "lint": {
+        "tp": 14,
+        "fp": 5,
+        "fn": 18,
+        "tn": 25,
+        "n": 62,
+        "recall": 0.4375,
+        "precision": 0.7368421052631579,
+        "false_flag_rate": 0.16666666666666666,
+        "f1": 0.5490196078431372,
+        "recall_ci": [
+          0.2816508596944317,
+          0.6067469796877387
+        ],
+        "false_flag_ci": [
+          0.07336434240351683,
+          0.33564705185680177
+        ],
+        "precision_ci": [
+          0.5120803155892935,
+          0.8819376166045982
+        ]
+      },
+      "compile_only": {
+        "tp": 29,
+        "fp": 24,
+        "fn": 3,
+        "tn": 6,
+        "n": 62,
+        "recall": 0.90625,
+        "precision": 0.5471698113207547,
+        "false_flag_rate": 0.8,
+        "f1": 0.6823529411764705,
+        "recall_ci": [
+          0.7578150066422116,
+          0.9675990373736805
+        ],
+        "false_flag_ci": [
+          0.6269395261897256,
+          0.9049502189759876
+        ],
+        "precision_ci": [
+          0.41453742646439184,
+          0.6734263183985253
+        ]
+      }
+    }
+  },
+  "role_flagged_by_new_verdict": {
+    "faithful": {
+      "n": 25,
+      "flagged": 16
+    },
+    "minor_drift": {
+      "n": 13,
+      "flagged": 13
+    },
+    "not_formalizable": {
+      "n": 3,
+      "flagged": 2
+    },
+    "wrong": {
+      "n": 24,
+      "flagged": 24
+    }
+  }
+}

experiments/P0-pilot/run_pilot.py

@@ -0,0 +1,218 @@
+"""Run the pilot detectors over the pilot items. Resumable; one JSON line per item.
+
+    python experiments/P0-pilot/run_pilot.py --items experiments/P0-pilot/data/items.jsonl \
+        --out experiments/P0-pilot/data/results.jsonl --dry-run          # no API calls: shows the plan
+    python experiments/P0-pilot/run_pilot.py --items ... --out ... --max-calls 400
+
+Detectors (all see the passage and/or the Lean code, never the human labels):
+  lint    static patterns on the projected simplex          (no LLM)
+  role    source-side simplex (LLM sees only the passage) aligned to the Lean simplex
+  judge   one LLM call that sees passage + Lean and says faithful / not
+  compile the stored Lean verdict (``verified``), read from the items file
+
+Hard stops: --max-calls bounds API calls; a rerun skips items already in --out.
+"""
+from __future__ import annotations
+
+import argparse
+import fcntl
+import hashlib
+import inspect
+import json
+import os
+import sys
+from pathlib import Path
+
+from leanbench import srcsimplex
+from leanbench.align import align
+from leanbench.config import Settings
+from leanbench.lint import lint
+from leanbench.llm import OpenAICompatibleClient, Usage
+from leanbench.project import project
+
+JUDGE_PROMPT_VERSION = "judge-v1"
+JUDGE_SYSTEM = (
+    "You check a Lean 4 (Mathlib) formalization against a textbook passage. Decide whether the "
+    "Lean statement says what the passage says: same objects, same hypotheses, same conclusion, "
+    "same quantifiers. Ignore whether it compiles. Reply with JSON only: "
+    '{"faithful": true|false, "confidence": 0..1, "reason": "one sentence"}'
+)
+
+
+def judge(client, passage: str, lean: str) -> dict:
+    reply = client.complete_json([
+        {"role": "system", "content": JUDGE_SYSTEM},
+        {"role": "user", "content": f"Passage:\n{passage}\n\nLean:\n{lean}"},
+    ])
+    if not isinstance(reply, dict) or type(reply.get("faithful")) is not bool:
+        raise ValueError(f"unusable judge reply: {str(reply)[:200]}")
+    return {"faithful": reply["faithful"], "confidence": reply.get("confidence"),
+            "reason": str(reply.get("reason", ""))[:300]}
+
+
+def run_item(client, item: dict) -> dict:
+    if not item.get("source_text", "").strip():
+        raise ValueError("Missing source_text; use a private source-inclusive export")
+    code = item.get("lean_code") or ""
+    row: dict = {"id": item["id"], "compiled": bool(item.get("verified")), "errors": {}}
+    proj = project(code)
+    row["projection"] = proj.as_dict()
+    row["lint"] = lint(proj)
+    try:
+        src = srcsimplex.extract_source_simplex(client, item.get("source_text", ""),
+                                                item.get("label", ""))
+        al = align(src, proj)
+        row["source"] = [r.__dict__ for r in src.roles]
+        row["role"] = al.as_dict()
+    except CallBudgetExceeded:
+        raise
+    except Exception as error:  # a failed extraction is data, not a crash
+        row["errors"]["role"] = str(error)[:300]
+    try:
+        row["judge"] = judge(client, item.get("source_text", ""), code)
+    except CallBudgetExceeded:
+        raise
+    except Exception as error:
+        row["errors"]["judge"] = str(error)[:300]
+    return row
+
+
+class CallBudgetExceeded(RuntimeError):
+    """Stop before issuing a request that would exceed the cumulative budget."""
+
+
+def digest(path: Path) -> str:
+    return hashlib.sha256(path.read_bytes()).hexdigest()
+
+
+def atomic_json(path: Path, value: dict) -> None:
+    temporary = path.with_suffix(path.suffix + ".tmp")
+    temporary.write_text(json.dumps(value, indent=2, allow_nan=False) + "\n", encoding="utf-8")
+    os.replace(temporary, path)
+
+
+class AuditedClient(OpenAICompatibleClient):
+    """Persist reservations before HTTP requests, including transport and JSON retries."""
+
+    def complete(self, *args, **kwargs):
+        try:
+            return super().complete(*args, **kwargs)
+        finally:
+            self.checkpoint()
+
+
+def execute(args, items, settings) -> int:
+    rows = []
+    if args.out.exists():
+        rows = [json.loads(x) for x in args.out.read_text(encoding="utf-8").splitlines() if x.strip()]
+    ids = {item["id"] for item in items}
+    done = {row["id"] for row in rows}
+    if len(done) != len(rows) or not done <= ids:
+        raise ValueError("Results have duplicate or unknown item IDs")
+    hashes = {
+        "source": hashlib.sha256((srcsimplex.SYSTEM_PROMPT + inspect.getsource(srcsimplex.passage_prompt)).encode()).hexdigest(),
+        "judge": hashlib.sha256(JUDGE_SYSTEM.encode()).hexdigest(),
+    }
+    identity = {"model": settings.llm.model, "base_url": settings.llm.base_url,
+                "temperature": settings.llm.temperature, "items_sha256": digest(args.items),
+                "prompt_hashes": hashes,
+                "prompts": [srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION]}
+    labels = getattr(args, "labels", None)
+    if labels is not None:
+        identity["labels_sha256"] = digest(labels)
+    meta_path = args.out.with_suffix(".meta.json")
+    meta = {**identity, "request_attempts": 0, "usage": Usage().as_dict(), "status": "ready"}
+    if meta_path.exists():
+        meta = json.loads(meta_path.read_text(encoding="utf-8"))
+        if any(meta.get(k) != v for k, v in identity.items()):
+            raise ValueError("Run identity changed; use a new output path instead of mixing runs")
+    elif rows:
+        raise ValueError("Cannot resume results without their audit metadata")
+    todo = [item for item in items if item["id"] not in done]
+    print(f"items={len(items)} done={len(done)} todo={len(todo)} model={settings.llm.model} "
+          f"nominal_calls={len(todo) * 2} request_attempts={meta['request_attempts']} cap={args.max_calls}")
+    print("prompt_hashes:", json.dumps(hashes))
+    if args.dry_run:
+        return 0
+    if settings.llm.model != "qwen-max" or settings.llm.temperature != 0:
+        raise ValueError("P0 is preregistered for qwen-max at temperature 0")
+    client = AuditedClient.from_settings(settings.llm)
+    client.usage = Usage(**meta["usage"])
+
+    def checkpoint():
+        meta["usage"] = client.usage.as_dict()
+        meta["completed_items"] = len(done)
+        atomic_json(meta_path, meta)
+
+    def reserve():
+        if meta["request_attempts"] >= args.max_calls:
+            raise CallBudgetExceeded("Cumulative request cap reached; no further HTTP request was sent")
+        meta["request_attempts"] += 1
+        checkpoint()
+
+    client.checkpoint = checkpoint
+    client.request_guard = reserve
+    meta["max_calls"] = args.max_calls
+    meta["status"] = "running"
+    checkpoint()
+    try:
+        with args.out.open("a", encoding="utf-8") as stream:
+            for item in todo:
+                row = run_item(client, item)
+                stream.write(json.dumps(row, ensure_ascii=False) + "\n")
+                stream.flush()
+                os.fsync(stream.fileno())
+                done.add(item["id"])
+                checkpoint()
+                print(f"completed={len(done)}/{len(items)} requests={meta['request_attempts']}", flush=True)
+        meta["status"] = "complete"
+    except CallBudgetExceeded as error:
+        meta["status"] = "budget_exhausted"
+        print(str(error), file=sys.stderr)
+    except BaseException:
+        meta["status"] = "interrupted"
+        raise
+    finally:
+        if args.out.exists():
+            meta["results_sha256"] = digest(args.out)
+        checkpoint()
+    print(json.dumps(meta))
+    return 0 if meta["status"] == "complete" else 2
+
+
+def main() -> int:
+    ap = argparse.ArgumentParser(description=__doc__.splitlines()[0])
+    ap.add_argument("--items", required=True, type=Path)
+    ap.add_argument("--out", required=True, type=Path)
+    ap.add_argument("--max-calls", type=int, default=400)
+    ap.add_argument("--dry-run", action="store_true")
+    ap.add_argument("--labels", type=Path, help="Frozen labels; their hash is bound to the run")
+    args = ap.parse_args()
+    if not 1 <= args.max_calls <= 400:
+        ap.error("P0 requires a request cap between 1 and 400")
+    items = [json.loads(x) for x in args.items.read_text(encoding="utf-8").splitlines() if x.strip()]
+    if not items or len({item["id"] for item in items}) != len(items):
+        ap.error("Input must contain unique item IDs")
+    if any(not item.get("source_text", "").strip() for item in items):
+        ap.error("Every item needs nonempty source_text; use a private source-inclusive export")
+    if not args.dry_run and args.labels is None:
+        ap.error("Freeze all blind labels first, then pass --labels")
+    if args.labels is not None:
+        annotation = json.loads(args.labels.read_text(encoding="utf-8"))
+        key_path = args.labels.with_name("key.json")
+        key = json.loads(key_path.read_text(encoding="utf-8"))["key"]
+        verdicts = {"faithful", "minor_drift", "wrong", "not_formalizable"}
+        if (set(key.values()) != {item["id"] for item in items}
+                or set(annotation["labels"]) != set(key)
+                or any(row.get("verdict") not in verdicts for row in annotation["labels"].values())
+                or annotation.get("items_sha256") != digest(args.items)
+                or annotation.get("key_sha256") != digest(key_path)):
+            ap.error("Frozen labels, key and source-inclusive items must be complete and match")
+    args.out.parent.mkdir(parents=True, exist_ok=True)
+    with args.out.with_suffix(args.out.suffix + ".lock").open("w") as lock:
+        fcntl.flock(lock, fcntl.LOCK_EX | fcntl.LOCK_NB)
+        return execute(args, items, Settings.from_env())
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

experiments/P0-pilot/score.py

@@ -0,0 +1,149 @@
+"""Score the pilot against frozen blind labels using the pre-registered decision.
+
+    python experiments/P0-pilot/score.py --results experiments/P0-pilot/data/results.jsonl \
+        --labels experiments/P0-pilot/labels/labels.json --key experiments/P0-pilot/labels/key.json --summary experiments/P0-pilot/results/summary.json
+
+Positive class = unfaithful. Primary: wrong versus faithful, excluding minor drift (role alignment and
+the judge do not need Lean to accept the code; only 10 of the 65 pilot items compiled, too few to
+decide on). Secondary: wrong or minor_drift; and the compiled-only subset (the paper's claim, reported
+with its interval, not used to decide). "not_formalizable" items are excluded. Decision (fixed before
+looking at labels):
+
+  GO       role recall on wrong items >= 0.5 AND false-flag rate on faithful items <= 0.2
+           AND role recall >= judge recall + 0.10 at a false-flag rate no higher than the judge's
+  PARTIAL  role recall >= 0.4 with false-flag <= 0.3, or role complements the judge
+           (flags >= 3 wrong items the judge misses)
+  NO-GO    otherwise (re-scope to evaluation + taxonomy + resource)
+With ~65 items every number carries a wide Wilson interval; the pilot checks for signal, not effect size.
+"""
+from __future__ import annotations
+
+import argparse
+import hashlib
+import json
+import math
+from pathlib import Path
+
+from leanbench.evalstats import auc, confusion, wilson
+
+
+def load(args):
+    result_rows = [json.loads(x) for x in args.results.read_text(encoding="utf-8").splitlines() if x.strip()]
+    results = {row["id"]: row for row in result_rows}
+    labels = json.loads(args.labels.read_text(encoding="utf-8"))["labels"]
+    key = json.loads(args.key.read_text(encoding="utf-8"))["key"]
+    if not key or len(set(key.values())) != len(key):
+        raise ValueError("The blind key must contain unique item IDs")
+    if len(results) != len(result_rows) or set(results) != set(key.values()):
+        raise ValueError("Results must cover every keyed item exactly once")
+    if set(labels) != set(key):
+        raise ValueError("Labels must cover every blind ID exactly once")
+    rows = []
+    for blind, item_id in key.items():
+        lab = labels.get(blind) or {}
+        if lab.get("verdict") not in {"faithful", "minor_drift", "wrong", "not_formalizable"}:
+            raise ValueError(f"Missing or invalid verdict for {blind}")
+        row = results[item_id]
+        if row.get("errors") or "judge" not in row or "role" not in row:
+            raise ValueError(f"Unresolved detector failure for {blind}; no decision can be issued")
+        rows.append({**row, "blind": blind, "verdict": lab["verdict"],
+                     "human_errors": lab.get("errors", [])})
+    return rows
+
+
+def flags(row):
+    return {
+        "compile_only": not row["compiled"],
+        "lint": bool(row.get("lint")),
+        "role": bool(row.get("role", {}).get("flagged")),
+        "judge": (not row["judge"]["faithful"]) if "judge" in row else False,
+    }
+
+
+def report(rows, positive):
+    out = {}
+    for name in ("compile_only", "lint", "role", "judge"):
+        out[name] = confusion([flags(r)[name] for r in rows], [positive(r) for r in rows]).as_dict()
+        out[name]["precision_ci"] = wilson(out[name]["tp"], out[name]["tp"] + out[name]["fp"])
+    out["role"]["auc_score"] = auc([-(r.get("role", {}).get("score", 1.0)) for r in rows],
+                                   [positive(r) for r in rows])
+    out["role"]["complementary_wrong"] = sum(
+        positive(r) and flags(r)["role"] and not flags(r)["judge"] for r in rows
+    )
+    return out
+
+
+def decide(sub):
+    role, judge = sub["role"], sub["judge"]
+    if role["tp"] + role["fn"] == 0 or role["fp"] + role["tn"] == 0:
+        return "INSUFFICIENT: both wrong and faithful items are required"
+    go = (role["recall"] >= 0.5 and role["false_flag_rate"] <= 0.2
+          and role["recall"] >= judge["recall"] + 0.10
+          and role["false_flag_rate"] <= judge["false_flag_rate"])
+    partial = ((role["recall"] >= 0.4 and role["false_flag_rate"] <= 0.3)
+               or role.get("complementary_wrong", 0) >= 3)
+    return "GO" if go else "PARTIAL" if partial else "NO-GO"
+
+
+def main() -> int:
+    ap = argparse.ArgumentParser(description=__doc__.splitlines()[0])
+    ap.add_argument("--results", required=True, type=Path)
+    ap.add_argument("--labels", required=True, type=Path)
+    ap.add_argument("--key", required=True, type=Path)
+    ap.add_argument("--summary", type=Path, default=None,
+                    help="also write the (text-free) summary here, e.g. results/summary.json")
+    args = ap.parse_args()
+    meta = json.loads(args.results.with_suffix(".meta.json").read_text(encoding="utf-8"))
+    if (meta.get("status") != "complete"
+            or meta.get("labels_sha256") != hashlib.sha256(args.labels.read_bytes()).hexdigest()
+            or meta.get("results_sha256") != hashlib.sha256(args.results.read_bytes()).hexdigest()):
+        ap.error("Scoring requires a complete run with unchanged frozen labels and results")
+    all_rows = load(args)
+    rows = [r for r in all_rows if r["verdict"] != "not_formalizable"]
+    primary = [r for r in rows if r["verdict"] != "minor_drift"]
+    compiled = [r for r in primary if r["compiled"]]
+    summary = {
+        "run_metadata": meta,
+        "n_labeled": len(all_rows), "n_evaluable": len(rows), "n_primary": len(primary),
+        "n_compiled": len(compiled),
+        "verdicts": {v: sum(r["verdict"] == v for r in rows) for v in
+                     ("faithful", "minor_drift", "wrong", "not_formalizable")},
+        "compiled_but_wrong": sum(r["verdict"] == "wrong" for r in compiled),
+        "primary_all": report(primary, lambda r: r["verdict"] == "wrong"),
+        "secondary_all": report(rows, lambda r: r["verdict"] in ("wrong", "minor_drift")),
+        "compiled_only": report(compiled, lambda r: r["verdict"] == "wrong"),
+    }
+    summary["verdicts"]["not_formalizable"] = len(all_rows) - len(rows)
+    summary["role_recall_by_error"] = {
+        error: {"flagged": sum(flags(r)["role"] for r in rows
+                                if r["verdict"] == "wrong" and error in r["human_errors"]),
+                "total": sum(r["verdict"] == "wrong" and error in r["human_errors"] for r in rows)}
+        for error in sorted({e for r in rows for e in r["human_errors"]})
+    }
+    summary["degenerate_projection"] = {
+        "total": sum(bool(r.get("projection", {}).get("degenerate")) for r in all_rows),
+        "wrong": sum(r["verdict"] == "wrong" and bool(r.get("projection", {}).get("degenerate"))
+                     for r in all_rows),
+    }
+    summary["disagreements"] = [
+        {"blind": r["blind"], "verdict": r["verdict"], "flags": flags(r)}
+        for r in primary if any(f != (r["verdict"] == "wrong") for f in flags(r).values())
+    ]
+    summary["decision"] = decide(summary["primary_all"])
+    def finite_json(value):
+        if isinstance(value, dict):
+            return {k: finite_json(v) for k, v in value.items()}
+        if isinstance(value, (list, tuple)):
+            return [finite_json(v) for v in value]
+        return None if isinstance(value, float) and not math.isfinite(value) else value
+
+    text = json.dumps(finite_json(summary), indent=2, allow_nan=False)
+    if args.summary:
+        args.summary.parent.mkdir(parents=True, exist_ok=True)
+        args.summary.write_text(text + "\n", encoding="utf-8")
+    print(text)
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())

experiments/pilot/README.md

@@ -1,15 +0,0 @@
-# Pilot (Phase 0)
-
-Question: on the 65 existing items, does role alignment (passage simplex vs. Lean simplex) find
-unfaithful formalizations better than a single LLM judge, compile-only, or static lint?
-Full protocol and decision rule: `docs/experiments/PROTOCOL.md`.
-
-    python experiments/pilot/make_sheet.py --items runs/p85-110/items.jsonl --out runs/pilot/private
-    # a person opens runs/pilot/private/labelsheet.html, labels all items, saves labels.json
-    python experiments/pilot/run_pilot.py --items runs/p85-110/items.jsonl --out runs/pilot/results.jsonl --dry-run
-    python experiments/pilot/run_pilot.py --items runs/p85-110/items.jsonl --out runs/pilot/results.jsonl
-    python experiments/pilot/score.py --results runs/pilot/results.jsonl \
-        --labels runs/pilot/private/labels.json --key runs/pilot/private/key.json
-
-`runs/` and `**/private/` are gitignored: the passages come from a copyrighted book and must not be
-committed. Labeling must finish BEFORE `score.py` is run; do not look at `results.jsonl` while labeling.

experiments/pilot/run_pilot.py

@@ -1,110 +0,0 @@
-"""Run the pilot detectors over the pilot items. Resumable; one JSON line per item.
-
-    python experiments/pilot/run_pilot.py --items runs/p85-110/items.jsonl \
-        --out runs/pilot/results.jsonl --dry-run          # no API calls: shows the plan
-    python experiments/pilot/run_pilot.py --items ... --out ... --max-calls 400
-
-Detectors (all see the passage and/or the Lean code, never the human labels):
-  lint    static patterns on the projected simplex          (no LLM)
-  role    source-side simplex (LLM sees only the passage) aligned to the Lean simplex
-  judge   one LLM call that sees passage + Lean and says faithful / not
-  compile the stored Lean verdict (``verified``), read from the items file
-
-Hard stops: --max-calls bounds API calls; a rerun skips items already in --out.
-"""
-from __future__ import annotations
-
-import argparse
-import hashlib
-import json
-import sys
-from pathlib import Path
-
-from leanbench import srcsimplex
-from leanbench.align import align
-from leanbench.config import Settings
-from leanbench.lint import lint
-from leanbench.llm import OpenAICompatibleClient
-from leanbench.project import project
-
-JUDGE_PROMPT_VERSION = "judge-v1"
-JUDGE_SYSTEM = (
-    "You check a Lean 4 (Mathlib) formalization against a textbook passage. Decide whether the "
-    "Lean statement says what the passage says: same objects, same hypotheses, same conclusion, "
-    "same quantifiers. Ignore whether it compiles. Reply with JSON only: "
-    '{"faithful": true|false, "confidence": 0..1, "reason": "one sentence"}'
-)
-
-
-def judge(client, passage: str, lean: str) -> dict:
-    reply = client.complete_json([
-        {"role": "system", "content": JUDGE_SYSTEM},
-        {"role": "user", "content": f"Passage:\n{passage}\n\nLean:\n{lean}"},
-    ])
-    if not isinstance(reply, dict) or "faithful" not in reply:
-        raise ValueError(f"unusable judge reply: {str(reply)[:200]}")
-    return {"faithful": bool(reply["faithful"]), "confidence": reply.get("confidence"),
-            "reason": str(reply.get("reason", ""))[:300]}
-
-
-def run_item(client, item: dict) -> dict:
-    code = item.get("lean_code") or ""
-    row: dict = {"id": item["id"], "compiled": bool(item.get("verified")), "errors": {}}
-    proj = project(code)
-    row["projection"] = proj.as_dict()
-    row["lint"] = lint(proj)
-    try:
-        src = srcsimplex.extract_source_simplex(client, item.get("source_text", ""),
-                                                item.get("label", ""))
-        al = align(src, proj)
-        row["source"] = [r.__dict__ for r in src.roles]
-        row["role"] = al.as_dict()
-    except Exception as error:  # a failed extraction is data, not a crash
-        row["errors"]["role"] = str(error)[:300]
-    try:
-        row["judge"] = judge(client, item.get("source_text", ""), code)
-    except Exception as error:
-        row["errors"]["judge"] = str(error)[:300]
-    return row
-
-
-def main() -> int:
-    ap = argparse.ArgumentParser(description=__doc__.splitlines()[0])
-    ap.add_argument("--items", required=True, type=Path)
-    ap.add_argument("--out", required=True, type=Path)
-    ap.add_argument("--max-calls", type=int, default=400)
-    ap.add_argument("--dry-run", action="store_true")
-    args = ap.parse_args()
-
-    items = [json.loads(x) for x in args.items.read_text(encoding="utf-8").splitlines() if x.strip()]
-    done = set()
-    if args.out.exists():
-        done = {json.loads(x)["id"] for x in args.out.read_text(encoding="utf-8").splitlines() if x.strip()}
-    todo = [i for i in items if i["id"] not in done]
-    settings = Settings.from_env()
-    est = len(todo) * 3  # extract (<=2 tries) + judge
-    print(f"items={len(items)} done={len(done)} todo={len(todo)} model={settings.llm.model} "
-          f"est_calls<={est} (extract x2 + judge) cap={args.max_calls}")
-    print("prompts:", srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION,
-          hashlib.sha256((srcsimplex.SYSTEM_PROMPT + JUDGE_SYSTEM).encode()).hexdigest()[:12])
-    if args.dry_run:
-        return 0
-
-    client = OpenAICompatibleClient.from_settings(settings.llm)
-    args.out.parent.mkdir(parents=True, exist_ok=True)
-    with args.out.open("a", encoding="utf-8") as fh:
-        for item in todo:
-            if client.usage.calls >= args.max_calls:
-                print("call cap reached; rerun to resume", file=sys.stderr)
-                break
-            fh.write(json.dumps(run_item(client, item), ensure_ascii=False) + "\n")
-            fh.flush()
-    meta = {"model": settings.llm.model, "usage": client.usage.as_dict(),
-            "prompts": [srcsimplex.PROMPT_VERSION, JUDGE_PROMPT_VERSION]}
-    (args.out.parent / "run_meta.json").write_text(json.dumps(meta, indent=2), encoding="utf-8")
-    print(json.dumps(meta))
-    return 0
-
-
-if __name__ == "__main__":
-    raise SystemExit(main())

experiments/pilot/score.py

@@ -1,93 +0,0 @@
-"""Score the pilot: detectors vs. the blind human labels, with the pre-registered decision.
-
-    python experiments/pilot/score.py --results runs/pilot/results.jsonl \
-        --labels runs/pilot/private/labels.json --key runs/pilot/private/key.json
-
-Positive class = unfaithful. Primary: verdict == "wrong", over ALL labeled items (role alignment and
-the judge do not need Lean to accept the code; only 10 of the 65 pilot items compiled, too few to
-decide on). Secondary: wrong or minor_drift; and the compiled-only subset (the paper's claim, reported
-with its interval, not used to decide). "not_formalizable" items are excluded. Decision (fixed before
-looking at labels):
-
-  GO       role recall on wrong items >= 0.5 AND false-flag rate on faithful items <= 0.2
-           AND role recall >= judge recall + 0.10 at a false-flag rate no higher than the judge's
-  PARTIAL  role recall >= 0.4 with false-flag <= 0.3, or role complements the judge
-           (flags >= 3 wrong items the judge misses)
-  NO-GO    otherwise (re-scope to evaluation + taxonomy + resource)
-With ~65 items every number carries a wide Wilson interval; the pilot checks for signal, not effect size.
-"""
-from __future__ import annotations
-
-import argparse
-import json
-from pathlib import Path
-
-from leanbench.evalstats import auc, confusion
-
-
-def load(args):
-    results = {json.loads(x)["id"]: json.loads(x) for x in args.results.read_text(encoding="utf-8").splitlines() if x.strip()}
-    labels = json.loads(args.labels.read_text(encoding="utf-8"))["labels"]
-    key = json.loads(args.key.read_text(encoding="utf-8"))["key"]
-    rows = []
-    for blind, item_id in key.items():
-        lab = labels.get(blind) or {}
-        if item_id in results and lab.get("verdict"):
-            rows.append({**results[item_id], "blind": blind, "verdict": lab["verdict"],
-                         "human_errors": lab.get("errors", [])})
-    return rows
-
-
-def flags(row):
-    return {
-        "compile_only": not row["compiled"],
-        "lint": bool(row.get("lint")),
-        "role": bool(row.get("role", {}).get("flagged")),
-        "judge": (not row["judge"]["faithful"]) if "judge" in row else False,
-    }
-
-
-def report(rows, positive):
-    out = {}
-    for name in ("compile_only", "lint", "role", "judge"):
-        out[name] = confusion([flags(r)[name] for r in rows], [positive(r) for r in rows]).as_dict()
-    out["role"]["auc_score"] = auc([-(r.get("role", {}).get("score", 1.0)) for r in rows],
-                                   [positive(r) for r in rows])
-    return out
-
-
-def decide(sub):
-    role, judge = sub["role"], sub["judge"]
-    if role["tp"] + role["fn"] == 0:
-        return "INSUFFICIENT: no wrong items in the labels"
-    go = (role["recall"] >= 0.5 and role["false_flag_rate"] <= 0.2
-          and role["recall"] >= judge["recall"] + 0.10
-          and role["false_flag_rate"] <= judge["false_flag_rate"])
-    partial = (role["recall"] >= 0.4 and role["false_flag_rate"] <= 0.3)
-    return "GO" if go else "PARTIAL" if partial else "NO-GO"
-
-
-def main() -> int:
-    ap = argparse.ArgumentParser(description=__doc__.splitlines()[0])
-    ap.add_argument("--results", required=True, type=Path)
-    ap.add_argument("--labels", required=True, type=Path)
-    ap.add_argument("--key", required=True, type=Path)
-    args = ap.parse_args()
-    rows = [r for r in load(args) if r["verdict"] != "not_formalizable"]
-    compiled = [r for r in rows if r["compiled"]]
-    summary = {
-        "n_labeled": len(rows), "n_compiled": len(compiled),
-        "verdicts": {v: sum(r["verdict"] == v for r in rows) for v in
-                     ("faithful", "minor_drift", "wrong")},
-        "compiled_but_wrong": sum(r["verdict"] == "wrong" for r in compiled),
-        "primary_all": report(rows, lambda r: r["verdict"] == "wrong"),
-        "secondary_all": report(rows, lambda r: r["verdict"] in ("wrong", "minor_drift")),
-        "compiled_only": report(compiled, lambda r: r["verdict"] == "wrong"),
-    }
-    summary["decision"] = decide(summary["primary_all"])
-    print(json.dumps(summary, indent=2, default=str))
-    return 0
-
-
-if __name__ == "__main__":
-    raise SystemExit(main())

leanbench/llm.py

@@ -14,7 +14,7 @@ import re
 import time
 import urllib.error
 import urllib.request
-from collections.abc import Iterable
+from collections.abc import Callable, Iterable
 from dataclasses import dataclass, field
 from typing import Any, Protocol
 
@@ -66,6 +66,7 @@ class OpenAICompatibleClient:
     max_retries: int = 4
     temperature: float = 0.0
     usage: Usage = field(default_factory=Usage)
+    request_guard: Callable[[], None] | None = field(default=None, repr=False)
 
     @classmethod
     def from_settings(cls, settings: LLMSettings) -> OpenAICompatibleClient:
@@ -97,6 +98,8 @@ class OpenAICompatibleClient:
         }
         last: Exception | None = None
         for attempt in range(self.max_retries + 1):
+            if self.request_guard is not None:
+                self.request_guard()
             request = urllib.request.Request(url, data=body, headers=headers, method="POST")
             try:
                 with urllib.request.urlopen(request, timeout=self.timeout) as response:

tests/test_assistant_diagnostic.py

@@ -0,0 +1,74 @@
+"""Current-chat review replay is offline, complete and text-free at its public boundary."""
+import copy
+import importlib.util
+from pathlib import Path
+
+import pytest
+
+PATH = Path(__file__).resolve().parents[1] / "experiments/P0-pilot/assistant_diagnostic.py"
+SPEC = importlib.util.spec_from_file_location("assistant_diagnostic", PATH)
+DIAG = importlib.util.module_from_spec(SPEC)
+SPEC.loader.exec_module(DIAG)
+
+ITEM = {"id": "synthetic", "source_text": "Synthetic private prose.",
+        "lean_code": "theorem t (n : Nat) : n = n := rfl", "verified": True}
+ASSESSMENT = {"records": [{"id": "synthetic", "blind_id": "P01", "source": {
+    "roles": [{"kind": "object", "symbols": ["n"], "description": "Private object wording",
+               "keywords": ["natural"]},
+              {"kind": "goal", "description": "Private goal wording", "keywords": ["equal"]}],
+    "goal_has_exists": False},
+    "judge": {"verdict": "faithful", "faithful": True, "errors": [],
+              "reason": "Private reviewer explanation"}}]}
+
+
+def test_offline_replay_and_text_free_public_output(monkeypatch):
+    def no_network(*args, **kwargs):
+        raise AssertionError("Replay must not call an API")
+
+    monkeypatch.setattr("urllib.request.urlopen", no_network)
+    rows = DIAG.evaluate([ITEM], {"P01": "synthetic"}, ASSESSMENT)
+    assert len(rows) == 1 and rows[0]["errors"] == {}
+    public = DIAG.public_items(rows, {"P01": {"verdict": "faithful"}})
+    assert public[0]["assistant_verdict"] == "faithful"
+    assert not any(word in str(public) for word in ["Private", "Synthetic", "explanation"])
+    assert all(key not in public[0] for key in ["source", "judge", "reason", "lean_code", "source_text"])
+
+
+def test_duplicate_or_missing_assessments_are_rejected():
+    assessment = copy.deepcopy(ASSESSMENT)
+    assessment["records"] *= 2
+    with pytest.raises(ValueError, match="Duplicate"):
+        DIAG.evaluate([ITEM], {"P01": "synthetic"}, assessment)
+    with pytest.raises(ValueError, match="same cohort"):
+        DIAG.evaluate([ITEM], {"P01": "synthetic"}, {"records": []})
+
+
+def test_mismatched_item_and_missing_source_are_rejected():
+    assessment = copy.deepcopy(ASSESSMENT)
+    assessment["records"][0]["id"] = "different"
+    with pytest.raises(ValueError, match="mismatched"):
+        DIAG.evaluate([ITEM], {"P01": "synthetic"}, assessment)
+    with pytest.raises(ValueError, match="Missing source"):
+        DIAG.evaluate([{**ITEM, "source_text": ""}], {"P01": "synthetic"}, ASSESSMENT)
+
+
+def test_judge_cannot_disagree_with_its_boolean_flag():
+    assessment = copy.deepcopy(ASSESSMENT)
+    assessment["records"][0]["judge"]["faithful"] = False
+    with pytest.raises(ValueError, match="Invalid authored judgment"):
+        DIAG.evaluate([ITEM], {"P01": "synthetic"}, assessment)
+
+
+def test_invalid_source_schema_is_rejected():
+    assessment = copy.deepcopy(ASSESSMENT)
+    assessment["records"][0]["source"]["roles"] = []
+    with pytest.raises(ValueError, match="goal"):
+        DIAG.evaluate([ITEM], {"P01": "synthetic"}, assessment)
+
+
+def test_agreement_is_explicitly_not_independent_and_has_no_gate():
+    rows = DIAG.evaluate([ITEM], {"P01": "synthetic"}, ASSESSMENT)
+    result = DIAG.agreement(rows, {"P01": {"verdict": "faithful"}})
+    assert result["metrics_are_non_independent_reference_agreement"] is True
+    assert "decision" not in result
+    assert DIAG.finite(float("nan")) is None

tests/test_pilot_scripts.py

@@ -2,7 +2,7 @@
 import importlib.util
 from pathlib import Path
 
-ROOT = Path(__file__).resolve().parents[1] / "experiments" / "pilot"
+ROOT = Path(__file__).resolve().parents[1] / "experiments" / "P0-pilot"
 
 
 def load(name):
@@ -36,3 +36,108 @@ def test_run_item_and_score(tmp_path):
     out = sc.report(rows, lambda r: r["verdict"] == "wrong")
     assert out["judge"]["n"] == 4
     assert sc.decide(out) in {"GO", "PARTIAL", "NO-GO"}
+
+
+def test_complementary_signal_is_partial():
+    sc = load("score")
+    rows = [
+        {"compiled": True, "lint": [], "role": {"flagged": i < 3, "score": 0.1},
+         "judge": {"faithful": False if 3 <= i < 8 else True}, "verdict": "wrong"}
+        for i in range(10)
+    ] + [
+        {"compiled": True, "lint": [], "role": {"flagged": False, "score": 1},
+         "judge": {"faithful": True}, "verdict": "faithful"}
+    ]
+    summary = sc.report(rows, lambda row: row["verdict"] == "wrong")
+    assert summary["role"]["recall"] == 0.3
+    assert summary["role"]["complementary_wrong"] == 3
+    assert sc.decide(summary) == "PARTIAL"
+
+
+def test_score_rejects_missing_labels_and_detector_failures(tmp_path):
+    import argparse
+    import json
+
+    import pytest
+
+    sc = load("score")
+    args = argparse.Namespace(results=tmp_path / "results.jsonl", labels=tmp_path / "labels.json",
+                              key=tmp_path / "key.json")
+    args.key.write_text(json.dumps({"key": {"P01": "x1"}}))
+    args.labels.write_text(json.dumps({"labels": {"P01": {"verdict": None}}}))
+    args.results.write_text(json.dumps({"id": "x1"}) + "\n")
+    with pytest.raises(ValueError, match="verdict"):
+        sc.load(args)
+    args.labels.write_text(json.dumps({"labels": {"P01": {"verdict": "wrong"}}}))
+    with pytest.raises(ValueError, match="detector failure"):
+        sc.load(args)
+    args.results.write_text("")
+    with pytest.raises(ValueError, match="every keyed item"):
+        sc.load(args)
+
+
+def test_request_budget_survives_resume_and_transport_retries(tmp_path, monkeypatch):
+    import argparse
+    import json
+    import urllib.error
+
+    import pytest
+
+    from leanbench.config import Settings
+
+    rp = load("run_pilot")
+    args = argparse.Namespace(items=tmp_path / "items.jsonl", out=tmp_path / "results.jsonl",
+                              max_calls=2, dry_run=False)
+    args.items.write_text(json.dumps(ITEM) + "\n")
+    monkeypatch.setenv("DASHSCOPE_API_KEY", "test-only")
+    settings = Settings()
+    settings.llm.max_retries = 5
+    requests = []
+
+    def fail(*args, **kwargs):
+        requests.append(1)
+        raise urllib.error.URLError("offline test")
+
+    monkeypatch.setattr("urllib.request.urlopen", fail)
+    monkeypatch.setattr("leanbench.llm.time.sleep", lambda *_: None)
+    assert rp.execute(args, [ITEM], settings) == 2
+    assert len(requests) == 2
+    assert rp.execute(args, [ITEM], settings) == 2
+    assert len(requests) == 2
+    meta = json.loads(args.out.with_suffix(".meta.json").read_text())
+    assert meta["request_attempts"] == 2
+    assert len(meta["prompt_hashes"]["judge"]) == 64
+    assert meta["status"] == "budget_exhausted"
+    settings.llm.model = "other-model"
+    with pytest.raises(ValueError, match="identity changed"):
+        rp.execute(args, [ITEM], settings)
+
+
+def test_run_rejects_missing_source_passage():
+    import pytest
+
+    rp = load("run_pilot")
+    with pytest.raises(ValueError, match="Missing source_text"):
+        rp.run_item(Stub(), {**ITEM, "source_text": ""})
+
+
+def test_restore_passages_checks_cohort_and_normalizes_archived_imports():
+    import pytest
+
+    prepare = load("prepare_items")
+    item = {"id": "x", "lean_code": "example : True := trivial", "imports": ["Mathlib"]}
+    original = {**item, "imports": '["Mathlib"]', "source_text": "A private passage."}
+    restored = prepare.restore([item], {"items": [original]})
+    assert restored == [{**item, "source_text": "A private passage."}]
+    with pytest.raises(ValueError, match="does not match"):
+        prepare.restore([{**item, "lean_code": "changed"}], {"items": [original]})
+
+
+def test_judge_rejects_string_boolean():
+    import pytest
+
+    from leanbench.llm import ScriptedClient
+
+    rp = load("run_pilot")
+    with pytest.raises(ValueError, match="unusable judge"):
+        rp.judge(ScriptedClient(['{"faithful": "false"}']), "passage", "code")