lean-bench/experiments/pilot/README.md

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.