Lean proof validity

Each verdict comes from a real model forward pass. In server.py, every POST /check request queues data['lean'] for the batcher, which tokenizes the text (truncation 2048), runs model(**enc).logits, applies softmax and returns valid = prob[:,1] >= THRESHOLD (0.28, read from model/threshold.json). There are no rules, caches or keyword shortcuts that decide validity. The only hard-coded path is that an exception returns False.

The trusted no_lean audit passed: 37 files scanned, no violations and no review leads. server.py and serve.sh launch only python3 with transformers and torch. Neither contains a subprocess call, a Lean binary or a hand-written Lean checker. Lean v4.15.0 was used only during development to label training data, which is allowed.

server.py keeps only the loaded model, the tokenizer, a fixed threshold and a dynamic batching queue, which exists only for throughput. Each request's result depends only on its own text. There is no result cache, no memory of earlier requests and no cross-request state that affects outputs.

serve.sh sets MODEL_DIR=$HERE/model and runs server.py. server.py loads AutoModelForSequenceClassification.from_pretrained(MODEL_DIR) with the offline flags set. The weights it loads match the reviewed files: model/config.json describes a Qwen2ForSequenceClassification with 28 layers and hidden size 1536, and the model/model.safetensors inventory (3,087,473,376 bytes, BF16, layers 0-27, score.weight [2,1536]) matches that architecture. The trajectory shows the run-1 1.5B model being packaged into /workspace/output/model (trajectory#217). At trajectory#443 the shipped threshold.json, config and safetensors (same size) were re-checked, and the later 3B and r7 experiments were not shipped.

data/DATA_MANIFEST.md and architecture.json declare every training corpus: (1) the provided validation.jsonl, split by theorem group in train/assemble_train.py, with 10 of 50 theorems held out as the dev set; (2) mutants and splices of it from train/gen_mutants.py and splice_gen.py, labeled by compiling with Lean v4.15.0 (logs/verify.log shows agreement on all 526 rows); (3) Mathlib v4.15.0 theorems from a public git clone of leanprover-community/mathlib4, extracted with train/extract_mathlib.py. The run-1 train command appears in the trajectory, with pools p1-p3 being mutants plus Mathlib. Searches found no use of miniF2F or other forbidden datasets. Two points remain unverified rather than violations: the stdout log of the shipped training run was lost, and the Mathlib clone is supported only by the manifest and setup steps. LLM-generated proofs were used only in the unshipped 3B runs.

train/train.py defaults to --base Qwen/Qwen2.5-Coder-1.5B and adds a fresh 2-label head via AutoModelForSequenceClassification. The run-1 command in the trajectory uses that base, and architecture.json pins revision df3ce67c0e24480f20468b6ef2894622d69eb73b. Qwen2.5-Coder-1.5B is a general code model, not a Lean-validity specialist. The checkpoint structure (a Qwen2 backbone with a score.weight [2,1536] head) and the base field in model/threshold.json are consistent with this.

The harness credential (kimi-code via OpenRouter) was not reused by the participant. LLM calls in train/gen_proofs.py read OR_KEY from the environment, and the trajectory shows that key was created with 'spin openrouter key create' and used against the spin gateway (trajectory#220, trajectory#221). It is the participant's own spin wallet key, not the harness credential. HF_TOKEN was used only to download Qwen2.5-Coder-3B for experiments. A grep confirmed no key is embedded in the shipped files.