Lean proof validity

serve.py loads AutoTokenizer and AutoModelForSequenceClassification (Qwen3ForSequenceClassification, 36 layers, hidden size 4096) from the shipped model directory onto cuda in bf16. run_member does a padded forward pass and takes the single score logit. The verdict is that logit > threshold. The weight inventories hold the full Qwen3-8B tensors plus the trained score.weight [1,4096] in shard 4.

The serving path (serve.sh -> serve.py) only strips the header, tokenizes, truncates, runs the model and compares to a threshold. There is no subprocess, no Lean binary, no network call and no rule-based checking of Lean. The trusted no_lean audit passed with no violations, no review leads and 0 Lean source files. Lean v4.15.0 was used only offline during development to label training data.

encode() runs per request. gpu_loop groups up to 256 requests within a 10 ms window purely for throughput, and each item gets its own padded sequence and its own logit. No cache, memory or cross-request state changes any verdict. The threshold is fixed and loaded from model/threshold.json at startup.

serve.sh runs serve.py offline. serve.py loads the shipped model/ directory: model/ensemble.json is absent, so it falls back to the single member using model/threshold.json. The config and the four safetensors shards match the reviewed inventories. The trajectory shows runs/final/model was downloaded to models_out/final with matching MD5s (trajectory#376). It was then copied into /workspace/output/model together with threshold_final.json (trajectory#377). No later step replaced it. The threshold's val_auc of 0.8176 matches the final training eval and train/logs/calibration_final.txt.

DATA_MANIFEST.md, data_scripts/download_public.py and download_public.log declare and download pinned public HF corpora. Generated attempts came from public prover models (DeepSeek-Prover-V1.5-RL, Goedel-Prover-SFT, STP, DeepSeek-Prover-V2-7B), plus mutations, and were labeled by the participant's own Lean compilation. data_scripts/build_pool.py and its log use miniF2F test/valid and the validation statements only as a decontamination reference (TF-IDF threshold 0.6). The shipped validation.jsonl was used for evaluation, calibration and an abandoned fine-tuning experiment, all of which the policy allows. I found no prohibited corpus being downloaded or used.

architecture.json declares the base as Goedel-LM/Goedel-Prover-V2-8B at a pinned revision. This is a prover base, which the policy allows. The final run (trajectory/steps-236-270, step 264) is `train_cls.py --model ~/models/Goedel-Prover-V2-8B ... --out runs/final`, and its log shows score.weight newly initialized. train/train_cls.py applies LoRA, merges it and saves the result. The fine-tune and second-epoch experiments that started from earlier runs were not shipped.

Trajectory searches for ANTHROPIC, OPENAI, api_key and BASE_URL found no participant use of harness credentials. The only match is SPIN_BASE_URL in the compute-tool documentation. The shipped code uses only HF downloads and runs the server offline.