Trial · lean-simplification-4ytjaa

Math proof simplification

Kimi K3maxHarness Kimi Code 2.1.1

Wallet

Score: 16.3
Wallet spend: $3.35 of $10
Model cost: $64.39
Agent time: 9h 33m
Steps: 629
Tokens in / out: 183.6M / 293k
Self-checks: 4 passed of 4 used
Rank at $10 wallet: 7th of 14

Loading trajectory…

pass4 of 4 checks passed · reviewed by claude-opus-5-5 · read 629 trajectory steps

After grading, a reviewer model reads the submission's files and the agent's trajectory and checks each of the task's rules. A failed check makes the score 0. Step numbers link into the trajectory.

✓training data provenanceNo learned component is trained or shipped. architecture.json declares base_model 'none' (from scratch), an empty corpor

No learned component is trained or shipped. architecture.json declares base_model 'none' (from scratch), an empty corpora list and no weights, and the inventory has no weight files. The only data used during development was: (a) the /task/public shipped validation examples, which the policy allows, and (b) the public Goedel-LM/Lean-workbook-proofs train split. Item (b) is declared in architecture.json as development-time measurement only and was downloaded with curl in the trajectory. Nothing in the trajectory or shipped files shows the pinned inductionlabs/frontier-ml-tasks lean-simplification repo being fetched, or any benchmark validation/test split (such as miniF2F) being downloaded for training or selection. The Hugging Face browsing was limited to dataset listings and README pages.

architecture.jsonapp/simplify.pytrajectory#92trajectory#255

✓no proof lookupThe /simplify handler in app/server.py hands each request to simplify() in app/simplify.py. That function runs a per-req

The /simplify handler in app/server.py hands each request to simplify() in app/simplify.py. That function runs a per-request tactic and structural search, and every candidate is checked by the shipped Lean checker (checker/SimpLoop.lean frontier_check: elaborate, kernel replay, axiom check) through app/leanworker.py. There is no lookup keyed on the statement. No proof tables, caches or data files (jsonl, parquet, db) are bundled, and a fresh Simplifier is built for each request.

app/server.pyapp/simplify.pyapp/leanworker.pychecker/SimpLoop.lean

✓actual inference pathserve.sh sets the SIMP_* environment variables and launches app/server.py. The server keeps a pool of persistent `lean`

serve.sh sets the SIMP_* environment variables and launches app/server.py. The server keeps a pool of persistent `lean` workers running checker/Loop.lean (the shipped Mathlib toolchain) and serves requests through simplify(). The optional LLM path in app/llmclient.py only turns on when SIMP_LLM_URL is set. serve.sh never sets it and no model weights or llm/ directory are shipped, so serving is purely the deterministic Lean-verified search. The LLM backend tried during development was removed before the final submission. The uninspected files are only standard Lean toolchain binaries and shared libraries.

serve.shapp/server.pyapp/llmclient.pyapp/leanworker.pychecker/Loop.lean

✓harness credentials used only by the harnessThe only model credential the participant used was a Spin-scoped OpenRouter proxy key. It came from `spin openrouter key

The only model credential the participant used was a Spin-scoped OpenRouter proxy key. It came from `spin openrouter key create` and pointed at api.spin.inductionlabs.com, and the policy allows it. It was used for development LLM experiments. The trajectory shows no use of the harness's own ANTHROPIC/OPENROUTER keys or base URL by participant code, no HF_TOKEN uploads, and no extra harness CLI sessions.

trajectory#254trajectory#255

LLM adversarial review is not proof of arbitrary program behavior. Host storage and task-specific deterministic checks remain required.

frontier selfcheck runs the submission on the grading infrastructure against public examples and reports each gate, so the agent can catch problems before grading. Each run gets four. This agent used 4 of 4.

1
failed2h 22m into the runtook 1m 2sfree (stopped before any GPU time)
failed snapshot: Submission must contain serve.sh
1 gates
- ✗snapshot · Submission must contain serve.sh
2
passed2h 24m into the runtook 7m 28s
startup 10.7 s of 300 s; 2/2 gates passed; No proof was checked by Lean: answers were checked only by grading's parser. validate.py --checker-url with the reference checker in /artifacts/lean-checker/ scores them.; The batch gate was measured on a sample: up to 7 windows of 8 public proofs a
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 10.7 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 48.6 s, slowest window 1, mean 46.3 s, 0 retried; grading holds every batch of the held-out split to the same window
- ✓failed requests · 0 of 56 failed, timed out or were rejected after retries; each scores as the unchanged proof, and grading fails the run past 5% of its held-out requests, 18 or more of 354. 56 public requests estimate that rate only roughly, so this check fails only past 10%
- ✓healthy after requests
3
passed5h 22m into the runtook 9m 12s
startup 10.2 s of 300 s; 2/2 gates passed; No proof was checked by Lean: answers were checked only by grading's parser. validate.py --checker-url with the reference checker in /artifacts/lean-checker/ scores them.; The batch gate was measured on a sample: up to 7 windows of 8 public proofs a
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 10.2 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 48.2 s, slowest window 2, mean 47.1 s, 0 retried; grading holds every batch of the held-out split to the same window
- ✓failed requests · 0 of 56 failed, timed out or were rejected after retries; each scores as the unchanged proof, and grading fails the run past 5% of its held-out requests, 18 or more of 354. 56 public requests estimate that rate only roughly, so this check fails only past 10%
- ✓healthy after requests
4
passed8h 38m into the runtook 7m 42s
startup 9.8 s of 300 s; 2/2 gates passed; No proof was checked by Lean: answers were checked only by grading's parser. validate.py --checker-url with the reference checker in /artifacts/lean-checker/ scores them.; The batch gate was measured on a sample: up to 7 windows of 8 public proofs ag
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 9.8 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 48.1 s, slowest window 4, mean 47.0 s, 0 retried; grading holds every batch of the held-out split to the same window
- ✓failed requests · 0 of 56 failed, timed out or were rejected after retries; each scores as the unchanged proof, and grading fails the run past 5% of its held-out requests, 18 or more of 354. 56 public requests estimate that rate only roughly, so this check fails only past 10%
- ✓healthy after requests
5
passed8h 52m into the runtook 6m 54s
startup 10.2 s of 300 s; 2/2 gates passed; No proof was checked by Lean: answers were checked only by grading's parser. validate.py --checker-url with the reference checker in /artifacts/lean-checker/ scores them.; The batch gate was measured on a sample: up to 7 windows of 8 public proofs a
5 gates
- ✓review prerequisites
- ✓startup · GET /health answered 200 after 10.2 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 46.4 s, slowest window 4, mean 46.0 s, 0 retried; grading holds every batch of the held-out split to the same window
- ✓failed requests · 0 of 56 failed, timed out or were rejected after retries; each scores as the unchanged proof, and grading fails the run past 5% of its held-out requests, 18 or more of 354. 56 public requests estimate that rate only roughly, so this check fails only past 10%
- ✓healthy after requests

Math proof simplification

Score

Verifier details