Math proof simplification
- Score
- 2.6
- Wallet spend
- $0.00 of $50
- Model cost
- $14.31
- Agent time
- 1h 4m
- Steps
- 995
- Tokens in / out
- 137.7M / 255k
- Self-checks
- 1 passed of 1 used
- Rank at $50 wallet
- 12th of 14
Score
2.6raw metric 0.02552
The score is the raw metric (mean proof-token reduction over proofs that still check), which already runs from 0 to 1, times 100.
Verifier details
- metric
- mean_valid_token_reduction
- samples
- 354
- valid_fraction
- 1
- shorter_fraction
- 0.0904
- standard_error
- 0.0053
- proof_checking_seconds
- 46.8523
- preflight_seconds
- 595.0966
- batch_budget_seconds
- 2700
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 provenanceNothing in the submission is trained. architecture.json declares base_model 'none' and lists no training evidence files,
Nothing in the submission is trained. architecture.json declares base_model 'none' and lists no training evidence files, and server.py contains only hand-written heuristics: single tactics, bracket deduplication, keeping only the terminal step, and removing unused have steps. The trajectory shows the participant built and tuned these heuristics only against /task/public/validation.jsonl, which is the shipped public example set and is allowed. I found no download of the inductionlabs/frontier-ml-tasks repository, the private folder, or any benchmark validation/test split. HF API calls only fetched metadata or configs for public models such as DeepSeek-Prover, and no model ships. The Lean runtime archive was assembled from the Lean v4.15.0 GitHub release, the mathlib4 v4.15.0 clone and its cache, and the task's ProofCheck checker.
✓no proof lookupThe POST /simplify handler in server.py calls simplify(statement, proof), which builds candidates at request time from t
The POST /simplify handler in server.py calls simplify(statement, proof), which builds candidates at request time from the request's own statement and proof. It checks each candidate by running the local Lean binary in a subprocess through lean_check. There is no table, index, cache or embedding store mapping statements to proofs, and no network access at serve time. The only bundled data are the lean_runtime.tar.zst archive and two wheels. The trajectory shows the archive holds only the Lean toolchain, mathlib build libs and ProofCheck.olean (trajectory#797, trajectory#801), and both wheels carry approved trusted audits.
✓actual inference pathserve.sh installs the vendored zstandard/zstd wheels, unpacks lean_runtime.tar.zst to /tmp/lean_runtime, checks the Lean
serve.sh installs the vendored zstandard/zstd wheels, unpacks lean_runtime.tar.zst to /tmp/lean_runtime, checks the Lean binary, and runs server.py with exec. server.py serves /health and /simplify through a ThreadingHTTPServer. The handler calls simplify(), which uses only local Lean subprocess checks. There are no model weights, no decoy checkpoint, no remote service, and no global state shared across requests. The trajectory records the end-to-end serve test from /submission (trajectory#830, trajectory#990 region).
✓harness credentials used only by the harnessSearching the trajectory found no step that reads, echoes or uses ANTHROPIC/OPENAI/OPENROUTER/GEMINI API keys or harness
Searching the trajectory found no step that reads, echoes or uses ANTHROPIC/OPENAI/OPENROUTER/GEMINI API keys or harness base URLs. There are also no calls to model APIs from participant code and no extra harness CLI sessions. The only Spin use is help output (trajectory#188). The provided read-only HF token was used only for read-only model metadata/config fetches (for example trajectory#193 region), which the policy allows.
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 1 of 4.
- 1passed58m 56s into the runtook 5m 45s
startup 18.9 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 18.9 s
- ✓slowest batch of 8 · 7 windows of 8 concurrent public proofs, the first straight after startup as in grading: first 35.6 s, slowest window 3, mean 37.2 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
The agent's last message before its session ended.
Submission Completed
The final solution has been validated with frontier selfcheck and submitted via frontier submit --confirm.
Summary of System Architecture and Performance
-
Self-Check Results (
45ba765d21daon NVIDIA H100 80GB HBM3):- Review prerequisites: PASSED
- Startup Latency: 18.9 s (limit: 300 s; 94% safety margin)
- Slowest Batch of 8 Requests: 39.12 s (limit: 60 s; 35% safety margin; mean batch time: 37.2 s)
- Failed Requests: 0% (0 of 56 failed; limit: 5%)
- Post-Request Health Check: PASSED
-
Artifacts Submitted in
/workspace/output/:serve.sh: Production-ready launch script that unpacks runtime assets, installs vendored dependencies, and starts the server on$HOST:$PORT.server.py: Multi-threaded HTTP server exposingGET /healthandPOST /simplify. Features a 4-phase simplification pipeline:- High-reward single-tactic solvers (
rfl,omega,ring,linarith,positivity,norm_num). - Bracketed argument deduplication.
- Compound terminal tactic reduction.
- Dead
haveelimination with backward dependency analysis. - Zero-risk fallback returning the original proof upon timeout or verification failure.
- High-reward single-tactic solvers (
architecture.json: Formatted provenance configuration.lean_runtime.tar.zst: Self-contained Lean 4.15.0 binary toolchain and pinned Mathlib oleans.wheels/: Vendored Python dependencies for offline installation.