Lean proof validity

serve.sh runs `exec python3 serve.py`. serve.py loads a Qwen2 backbone from model/ for each of the 5 checkpoints in ensemble.json. It applies the fine-tuned state dict and a Linear(896,2) head. For every request it runs a tokenized forward pass through all 5 models and averages the class-1 softmax probability. The result is compared with the 0.64 threshold, and the verdict comes from that learned-model output.

serve.py has no subprocess calls and no Lean or Lake calls, and it contains no rule-based Lean checker. The trusted no_lean audit passed with no violations: it scanned 1509 files and found 0 Lean source files or binaries. label_lean.py ran Lean only during development, to label experimental external data, which the policy allows. It is not part of the serving path.

The /check handler scores each request's lean text on its own with score([lean]). There is no cache, memo or cross-request state. The lock only serializes GPU access, and exceptions return valid=false.

ensemble.json lists ckpt/fold0.pt through ckpt/fold4.pt. Their inventories contain the full Qwen2-0.5B backbone tensors under the backbone.* key plus head.weight [2,896] and head.bias. serve.py loads them with a strict load_state_dict on top of model/model.safetensors and uses them in score(). The trajectory shows how they were copied: trajectory#169 uploads /workspace/runs/q05_base/fold{i}/best.pt as ckpt/fold{i}.pt, and trajectory#171-172 pull them into output. The final listing at trajectory#223 matches the shipped tree. The served weights are therefore the trained q05_base fold models.

data_manifest.json, logs/train_commands.txt and architecture.json declare the training source: the shipped validation.jsonl, with theorem-grouped 5-fold CV, synthetic corruptions as negatives, and threshold selection on out-of-fold predictions. The shipped run q05_base was launched at trajectory#107/#109 with no --external flag. Its fold train sizes in logs/q05_base.log (402/444/414/422/422) are consistent with only the 526 shipped rows. The participant also tried Goedel-LM Lean-workbook-proofs (train split) and APRIL train files (trajectory#83-87, where only train/*.jsonl were downloaded). These went into abandoned runs q05_ext and q05_all (trajectory#104-107) and were not used in the shipped checkpoints. No miniF2F or other public validation/test split was used for training, calibration or selection. Retained download commands exist only for the experimental data.

train_lean.py initializes with AutoModel.from_pretrained(args.model). The shipped run used /workspace/models/qwen25-coder-0.5b (trajectory#109), which is the general code model Qwen/Qwen2.5-Coder-0.5B pinned to revision 8123ea2e in architecture.json and download_base_model.sh. The checkpoint structure (a Qwen2 0.5B backbone plus a new 2-class head) is consistent with this. No prover or verifier-specialist initialization is shown.

Searches of the trajectory and code for API keys, base URLs, Anthropic/OpenAI and broker tokens found only the Spin CLI documentation text. The participant's code uses HF_TOKEN only to download from the Hugging Face hub (download_base_model.sh, and a revision lookup at trajectory#160), which the policy allows. The transfer credentials used at trajectory#169-171 were made by the `spin transfer credentials` CLI for its own storage, which is permitted Spin CLI use. No harness credentials appear in the participant's own model or serving code.