Math proof simplification

Nothing in the submission is trained. architecture.json says base_model "none" / "from-scratch" with no training evidence files, DATA.md says no training, fine-tuning, calibration or selection was done, and no weight inventory exists. The hand-written rewrite heuristics in simplify.py were tuned against /task/public/validation.jsonl, as the scoring runs in the trajectory show (trajectory#9, #94, #100, #101). Those are the shipped public examples, which the policy explicitly allows. The trajectory shows no download of the pinned inductionlabs dataset repository, no held-out data, and no validation or test split of any other public benchmark. The only shipped artifacts are Lean toolchain and Mathlib oleans, whose sources DATA.md declares.

The POST /simplify handler (do_POST -> simplify_one) builds candidate proofs at request time from the request's own proof text, using regex rewrites, duplicate-lemma removal and line drops (compact_rewrites and structural_candidates). Each candidate is accepted only if the warm Lean REPL checks it against the request's statement. There is no table, cache, index or embedding keyed by theorem statement. Apart from the code, the shipped files are Lean binaries and .olean libraries (Mathlib, Aesop, batteries, the REPL, and one FrontierCheck/ProofCheck.olean that is on LEAN_PATH but never imported). No JSONL, pickle or database files are shipped. The code makes no network calls; the only subprocess is the local REPL.

serve.sh sets environment variables and runs `python3 simplify.py`. main() starts a pool of LEAN_WORKERS REPL processes from the bundled lean/bin/repl, each importing Mathlib and Aesop, then serves the handler. Each request takes a REPL from the pool and runs simplify_one, which calls repl.check, which sends `example {statement} := {cand}` to Lean. If nothing checks in time, the original proof is returned. There is no model, decoy checkpoint, remote service or alternate path. The only state carried between requests is the warm REPL base environment and its use counters, which do not change answers based on earlier requests. The REPL binary was not inspected, but nothing in the evidence shows it doing anything beyond ordinary REPL use.

The session's commands only edit simplify.py, start the local server, score against public examples with urllib on 127.0.0.1, and run frontier selfcheck/submit (e.g. trajectory#93, #96, #102, #104). Searches of the trajectory found no use of *_API_KEY or *_BASE_URL variables, no model API calls, no curl or git clone downloads, and no extra harness CLI sessions.