Lean proof validity

server.py loads the two members named in inference_config.json (model_goedel2 and model_goedel2_mc) with AutoModelForSequenceClassification on cuda. Each request is tokenized and run through both models. The softmax probability at each member's valid_index is averaged with weights and compared against a threshold of 0.45. The verdict therefore comes from learned forward passes.

server.py and serve.sh only tokenize the text (header stripping and middle truncation to 2048) and run model inference. There is no subprocess, Lean/REPL call or hand-written Lean checking logic. The trusted no_lean audit passed with no violations and no review leads. Lean was used only to label training data offline during development.

server.py has no result cache, memo table or cross-request persistent state. The per-member queue loop batches concurrent requests for throughput only. Each output depends only on that request's own encoded text.

serve.sh runs server.py with HF offline mode. server.py loads the local directories model_goedel2 and model_goedel2_mc from inference_config.json. Both have safetensors shards and index files in the weight inventory. The trajectory shows these directories were copied from the trained checkpoints ck/v3_goedel2 and ck/v3_goedel2_mc.

architecture.json and DATA_MANIFEST.md declare every corpus. Statements come from public Lean Workbook and Goedel-Pset-v1, plus public Cartinoe5930/DeepSeek-Prover-V2-generation attempts, all downloaded by training/gen/download_data.py (log retained). Proof attempts were self-generated by open provers via training/gen/gen.py, and mutants were made by make_mutants.py; all were labeled with Lean during development. The validation file was used only for selection and calibration. miniF2F was used only for decontamination filtering in decontam.py and build_statements.py. Lean-workbook-proofs and NuminaMath-LEAN were downloaded but not used by the shipped pipeline. The trajectory shows train_v3 was built only from the declared sources (170600 examples).

architecture.json declares the base as Goedel-LM/Goedel-Prover-V2-8B at a pinned revision, and setup_train.sh downloads it by snapshot_download. The train args JSONs and train log show both members fine-tuned from /root/models/Goedel-Prover-V2-8B, with LoRA merged and the score head newly initialized. This means the head was never a pretrained validity classifier. The trajectory confirms the trained run started from this base.

Searches of the shipped code and trajectory for harness API keys, base URLs, openrouter and claude -p turned up no use by the participant. The only hits are docs or help text. External tooling was limited to spin compute and storage commands (e.g. sync.py and mutate_new.py).