Lean proof validity

serve.py loads the model with AutoModelForSequenceClassification.from_pretrained(MODEL_DIR). Each request is tokenized with head+tail truncation, padded and run through a forward pass. The verdict is softmax P(valid) compared against the learned threshold in model/calib.json. model/config.json declares Qwen3ForSequenceClassification with num_labels=2. No rule-based verdict path was found; on error the code falls back to a constant 0.5 probability.

Neither serve.py nor serve.sh calls a subprocess, Lean, Mathlib, olean files or hand-written checker rules. serve.sh only installs vendored wheels with --no-index and runs serve.py. The trusted no_lean audit passed with no violations and no review leads. Lean v4.15 was run only during development to produce training labels (DATA_MANIFEST.md, trajectory#494).

serve.py scores each /check request independently through async dynamic batching. Batching only groups concurrent requests into one forward pass. There is no result cache, no cross-request statistics and no adaptive state; the threshold is a constant read from calib.json at load time.

serve.sh sets MODEL_DIR=$(pwd)/model and serve.py loads from that directory. The shipped sharded safetensors (index plus model-00004 with layer 35, model.norm and score.weight [2,4096]) match the merged full checkpoint. That checkpoint was produced by pipeline_src/merge_model.py via merge_and_unload (trajectory#491–492) and downloaded into output/model (trajectory#500). No alternate weights or remote inference path was found.

DATA_MANIFEST.md and pipeline_src/prep_candidates.py declare the public train splits Goedel-LM/Lean-workbook-proofs and Goedel-LM/SFT_dataset_v2 as sources. Candidates are mutated, then labeled by development-time Lean compiles; label counts are in training_logs/labeling_summary.json. miniF2F (cloned in trajectory#29) is used only for 8-gram decontamination in pipeline_src/decontaminate.py, which is allowed. validation.jsonl was used only for external eval and threshold selection, which is allowed (trajectory#448, trajectory#492). Retained download logs exist only in the trajectory; the sources are public and declared.

train.py loads the base with from_pretrained(args.model, num_labels=2) and adds PEFT LoRA r=32. The final run (trajectory#448) used --model Goedel-LM/Goedel-Prover-V2-8B, an allowed general proof-generation base. training_logs/train_g30.log shows score.weight newly initialized from Goedel-LM/Goedel-Prover-V2-8B, and the merge in trajectory#491 uses the same base. No specialist Lean-validity checkpoint was used.

The trajectory shows HF_TOKEN used only for Hugging Face searches and downloads (trajectory#19) and Spin CLI compute and transfer-credential commands used for remote GPUs and S3 transfers (trajectory#497–500). Both are allowed. No harness CLI launch or use of API keys by the participant was found; searches for API_KEY and BASE_URL matched only Spin documentation text.