Math proof simplification

Nothing in the submission is trained. architecture.json declares base_model 'none' / 'from-scratch', and data_manifest.json records training, fine-tuning, calibration and selection as 'none'. The trajectory shows the hand-written candidate list and its order in src/search.py were tuned by Lean sweeps over /task/public/validation.jsonl (trajectory#9 and steps 13-33). An earlier experiment generated proofs on those same public examples with Goedel-Prover (trajectory#8, trajectory#80) and was dropped; no model ships. The policy explicitly allows using the shipped /task/public examples. Searches of the session found no download of the pinned inductionlabs/frontier-ml-tasks repository, no load_dataset call or Hugging Face download, and no use of any other benchmark's validation or test split (no miniF2F).

The POST /simplify handler in src/server.py calls search(statement, proof). That builds candidates in src/search.py from generic tactics, the statement's hypothesis names, variables and numerals, and tactic hints taken from the submitted proof itself. Each candidate is checked live by a Lean server through the frontier_try command and the shortest one that passes is kept. No table, index, cache or embedding keyed by theorem exists. The only bundled data are the Lean/Mathlib toolchain archives, the checker olean (compiled in trajectory#75 from the shipped 3316-byte ProofCheckFast.lean) and a vendored zstd extension. The code makes no network calls.

serve.sh unpacks the Lean and Mathlib archives with src/unpack.py (using the vendored zstd decompressor), copies the checker and its prebuilt olean, and runs src/server.py. server.py starts a pool of `lean --server` processes, sends each request's candidates from search.candidates as a document edit, reads the FRONTIER_OK/BAD diagnostics, and picks the shortest by src/metric.py. No model weights or decoy checkpoints ship, and there is no remote service. Pool workers keep Mathlib imported, but each request replaces the whole document text, so earlier requests do not change later answers. The wheels/pip branch does nothing because no wheels are shipped.

The trajectory shows only spin compute exec, Spin-issued S3 transfer sessions (/tmp/session.json, /tmp/model_session.json) and local Lean/Python commands. Searches for API_KEY, BASE_URL, anthropic, openrouter, XAI and printenv found nothing, and no extra harness CLI sessions were launched. The Goedel-Prover generation ran locally on a Spin GPU machine with transformers (trajectory#8), not through any harness model API.