Lean proof validity

serve.sh runs `exec python3 serve.py`. serve.py loads ./model with AutoModelForSequenceClassification (Qwen2ForSequenceClassification, bf16). Each POST /check takes data["lean"], tokenizes it (head 1024 + tail 256 tokens) and runs a model forward pass. The verdict is softmax[:,1] > THRESHOLD, with the threshold read from model/threshold.json (0.55). The prediction comes from the learned model, not from rules.

The trusted no_lean audit passed: 33 files scanned, no violations, no uninspected files, no review leads. serve.py has no subprocess, network, Lean or rule-based checker. Lean appears only in development-time labeling (docs/label.py runs `lake env lean` on the rented GPU box), which is not part of serving.

serve.py uses a queue-based dynamic batching worker (up to 48 requests per batch) only for throughput. Each request's verdict depends only on its own logits. There is no cache, memo, cross-request statistic or answer state, and errors return False. The end-to-end server test (trajectory#188) shows plain per-request responses.

serve.py loads ./model, which holds model/config.json (Qwen2ForSequenceClassification: 28 layers, hidden size 1536, vocab 151936) and model/model.safetensors. The weight inventory (3.09 GB BF16) contains the full Qwen2 stack plus a score.weight head of shape [2,1536], which matches the loader. The trajectory shows ckpt_v3 assembled with threshold.json (trajectory#187), served and smoke-tested (trajectory#188), uploaded to Spin storage, and copied into /workspace/output/model (trajectory#198). The packaging step records the sha256 of the shipped model.safetensors.

docs/DATA_MANIFEST.md and docs/download_data.py declare these sources: Goedel-LM/Lean-workbook-proofs (train split; 3500 gold proofs, plus mutations, canned tactics and cross-proof negatives labeled by Lean); internlm/Lean-Workbook lean_workbook.json (statements for LLM prover attempts); attempts from DeepSeek V3.2 and Qwen3 via Spin OpenRouter; gen2 mutations; and the 526 provided validation.jsonl rows. All are allowed. miniF2F (cat-searcher/minif2f-lean4 test/validation) was downloaded only to build a digit-normalized exclusion set. gen_attempts.py and extract_stmts.py (trajectory#54) put miniF2F statements in `bans` and drop matches; gen_attempts logged 'dropped_minif2f_overlap: 0' (trajectory#50). The downloads appear in the trajectory (#27, #29, #30), so the sources are declared and allowed. Nothing in the retained evidence leaves a corpus unverified.

train2.py defaults BASE to Qwen/Qwen2.5-Coder-1.5B, a general code base model, as declared in architecture.json (revision df3ce67c...). train2_v1.log and train_v2b.log both show 'newly initialized from the model checkpoint at Qwen/Qwen2.5-Coder-1.5B: [score.weight]'. The final v3 run continued from the participant's own ckpt_v2 (SKIP_HEAD_INIT=1, trajectory step 155 and the v3 launch in trajectory/steps-136-177); ckpt_v2 itself was trained from the Qwen2.5-Coder base. No specialist validity or verifier checkpoint was used.

The OpenRouter key used by llm_gen.py and llm_gen2.py (OR_KEY) was created with the participant's `spin openrouter key create` (trajectory#56, #57), which is allowed Spin proxy use. HF_TOKEN was used only for Hugging Face downloads on the Spin box (trajectory#27, #30). Spin S3 session credentials were used only to transfer the model through Spin storage (trajectory#198). Searches for ANTHROPIC, API_KEY and OPENROUTER found no use of the harness's own model credentials.