Math proof simplification

Nothing in the shipped system is trained, fine-tuned or calibrated. architecture.json declares training "none" and an empty training_data list, and provenance/README.md says the same. The only corpora used are Mathlib and the Lean toolchain, both as the checking environment, plus /task/public/validation.jsonl, the shipped public examples, which were used to test the server and tune its time budget (BUDGET_TUNING.md). The trajectory shows the participant inspecting public validation rows while designing the hand-written heuristics (trajectory#265, trajectory#266). That is allowed. A pretrained Goedel-Prover-V2-8B checkpoint was downloaded and tested as an optional proposer on the public examples only (trajectory#262, trajectory#263). It was never fine-tuned, was moved out of the output directory (trajectory#264) and was not shipped. Searches of the evidence found no download of the pinned dataset repository (inductionlabs/frontier-ml-tasks / lean-simplification), no load_dataset calls and no use of another benchmark's validation or test split.

server.py's POST /simplify handler calls simplify_guarded, which runs a SimplifyJob (simplify.py). The job builds candidate proofs at request time from the request's statement and proof: a fixed list of tactics to try (tactic battery), hints mined from the input proof, 'Try this:' suggestions from Lean, and structural edits such as deleting or replacing chunks. Each candidate is checked by the Lean worker pool (lean_pool.py) and kept only if it is valid and strictly shorter. The only state shared across requests is ResultCache, which maps (statement, candidate text) to a Lean verdict. It memoizes checks and never supplies a prepared proof. Apart from the Lean/Mathlib oleans, the shipped files are source code, provenance logs and evaluation logs. There are no JSONL, pickle, SQLite or embedding files and no network calls in the serving code. The code also avoids tactics that would reach the network (exact?, apply?, rw?).

serve.sh runs server.py, which builds a LeanPool of bin/checker_worker processes and a Simplifier. bin/checker_worker is a native binary with no trusted audit. Its source is shipped (provenance/checker_src/Worker.lean), and provenance/worker_build.log records building it with lake plus a smoke test. Nothing shows it doing anything beyond checking proofs. neural.py only turns on if $DIR/model exists. No model directory or wheels are shipped: the file inventory has no model or wheel files, the weight inventory is empty, and the model was moved out of the output directory before submission (trajectory#264, trajectory#313). So the propose callback is None and every answer comes from the heuristic engine plus Lean checks. No remote service is called. The cross-request ResultCache only stores Lean verdicts, so it saves time without supplying answers.

Searching the trajectory found no use of ANTHROPIC/OPENAI/OPENROUTER keys or the harness base URLs in the participant's own commands. It also found no SDK calls and no launches of extra claude, codex or similar CLI sessions. The only API_KEY and BASE_URL matches are in Spin CLI help text. HF_TOKEN appears in a script that downloads a model, which is allowed (trajectory#144-162 region; trajectory#260). The final audit step scanned the output directory for leaked tokens (trajectory#310).