Lean proof validity

server.py loads model32 with AutoModelForSequenceClassification (a Qwen3 model with a 2-class score head). For each request it tokenizes the Lean text, runs the forward pass and applies a softmax. It returns valid = p(class 1) >= the fixed threshold from inference_config.json. The weight inventory shows full Qwen3-32B BF16 weights, including score.weight [2,5120].

server.py makes no subprocess calls, does not call Lean or a REPL, and contains no rule-based checker. serve.sh only installs fastapi/uvicorn from local wheels and starts server.py. The trusted no_lean audit passed with no violations, 0 Lean source files and no review leads. Lean was used only during development to label training data, which is allowed.

In server.py, each /check result depends only on that request's body['lean'] passed through the fixed model and threshold. The async worker groups queued requests into batches only for throughput. There is no cache or state carried across requests.

serve.sh runs server.py with HF_HUB_OFFLINE=1. server.py reads inference_config.json, whose only model entry is model32 with weight 1.0, and loads ROOT/'model32' with local_files_only. The shipped model32 safetensors shards, config.json and index match the reviewed inventory. The trajectory shows how model32 was produced: base32 merged with the final32/epoch_3 adapter and moved into output/model32, with the earlier preflight models archived.

data_manifest.json and architecture.json declare the training sources: the 526 provided validation rows, AI-MO/NuminaMath-LEAN at a pinned revision (train split, source=math_train only), and the participant's own Lean-labeled generations. training/download_data.py and training/download_manifest.json keep the download commands and hashes. miniF2F (DeepSeek-Prover-V1.5 minif2f.jsonl) is read only in training/prepare_data.py, to build n-gram exclusion references for decontamination. It is never used as training or selection data.

The initialization is Goedel-LM/Goedel-Prover-V2-32B at a pinned revision, downloaded by training/download_comparison_model.py. This is a general proof-generation model, which the policy allows, not a validity classifier. training_source.py builds a fresh 2-label sequence-classification head on this base and adds LoRA. The run scripts chain base32 → foundation32 → foundation32_v2 → final32, and the trajectory shows the final merge used base32 plus the final32 epoch_3 adapter.

Searches of the trajectory for API_KEY, BASE_URL, OPENAI and ANTHROPIC returned no matches. No step uses, copies or ships harness credentials. A secret-pattern scan of the output directory at step 623 found nothing, and server.py makes no external API calls.