Lean proof validity

server.py loads AutoModelForSequenceClassification from the 'model' directory named in inference_config.json. For each proof it builds the fixed prompt from preprocessing.py, runs one forward pass, takes logits[:,1]-logits[:,0] and compares the result with the -0.15 threshold. The verdict comes directly from the learned score head (score.weight [2,4096]) of a 36-layer Qwen3 classifier. preprocessing.py only formats text (it renames the first theorem to 'target' and adds the prompt). It applies no heuristic that decides validity.

The trusted no_lean audit passed with 0 violations, 0 review leads and nothing left uninspected. server.py and serve.sh make no subprocess calls, invoke no Lean or Lake binary, make no network calls and contain no reimplementation of Lean checking. The trusted binary audits show wheels/ holds only web-serving packages (fastapi, uvicorn, pydantic, starlette, etc.). The Lean 4.15 compiler was used only on development machines to label training data, which data_manifest.json and the trajectory both describe as development-only.

server.py scores each request's text on its own. Dynamic batching groups requests by length and uses right padding with an attention mask, so it only affects throughput. There is no cache, memoization, cross-request state or label lookup, and the output for each row depends only on that row's tokens.

The serving path is serve.sh → exec python server.py → inference_config.json (models: [{path:'model', float16, weight 1.0}]) → model/config.json (Qwen3ForSequenceClassification) → model/model-0000{1..4}-of-00004.safetensors. The weight inventory shows these shards hold an F16 Qwen3 backbone plus score.weight, which matches the config. No other checkpoint, download or remote model is loaded at inference, and the environment is set to offline.

data_manifest.json declares every training source: (1) Lean-workbook-proofs and Goedel-Pset-v1 train splits at pinned revisions, downloaded by training/download_sources.py; (2) the shipped 526 validation rows and statements derived from them; (3) proof attempts generated with Spin/OpenRouter deepseek-v3.2 (training/generate_attempts.py) and labelled by a development-only Lean compiler; (4) internal calibration from unused workbook-train groups. miniF2F Test/Valid is cloned at a pinned commit (training/download_exclusions.sh) and used only as an exclusion filter (training/prepare_sources.py, training/make_pset_candidates.py). The overlap audits in the trajectory found no contamination. Every source is declared, and download commands or logs are retained.

architecture.json declares the base as Goedel-LM/Goedel-Prover-V2-8B at revision dfd02e62…. training/download_sources.py and logs/gpu_setup_and_model_download.log record the download at that pinned revision. The training logs show the whole chain (aux_mixed2 → aux_paired2/snapshot400 → final8_usergen50_seed3203) starting from auxdata/base or auxfresh/base, and the trajectory identifies both as Goedel8B, with auxfresh pinned to dfd02. Goedel-Prover is a proof generator, not a proof-validity classifier. training/train_auxiliary.py builds a new 2-class score head from the lm_head rows for ' invalid'/' valid' and trains it with LoRA, so the starting point was not a specialist verifier checkpoint.

The trajectory shows the participant created a separate OpenRouter key with `spin openrouter key create` and saved it to openrouter_key.json. training/generate_attempts.py reads that file through --credentials and is the only code that calls an LLM API. No shipped code or trajectory command reads OPENAI_*/harness API key or base-URL variables, and the participant never launched the agent harness CLI. The harness credentials were therefore not reused for the participant's own API calls.