Lean proof validity
- Score
- 0.0
- Wallet spend
- $2.00 of $10
- Model cost
- $3.81
- Agent time
- 2h 29m
- Steps
- 93
- Tokens in / out
- 8.5M / 50k
- Self-checks
- 1 passed of 2 used
- Rank at $10 wallet
- 12th of 14
Score
0.0raw metric 0.3969
The raw metric (macro F1) is rescaled so that a coin flip (macro F1 0.5) scores 0 and perfect classification scores 100, clamped to that range.
Verifier details
- metric
- macro_f1
- samples
- 3540
- theorems
- 295
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.
✓learned model forward passThe POST /check handler in app.py tokenizes r.lean (truncated to 1024 tokens), runs AutoModelForSequenceClassification o
The POST /check handler in app.py tokenizes r.lean (truncated to 1024 tokens), runs AutoModelForSequenceClassification on it and returns valid = (logits.argmax == 1). The answer comes from the model's forward pass. No rules or regexes produce the prediction.
✓no lean execution or reimplementationapp.py and serve.sh only import torch, transformers and fastapi, and only install fastapi and uvicorn from the bundled w
app.py and serve.sh only import torch, transformers and fastapi, and only install fastapi and uvicorn from the bundled wheels. There are no subprocess or network calls to Lean tools and no code that emulates tactics. The trusted no_lean audit passed with no violations and no review leads. setup_lean.sh and the Lean labeling runs (trajectory#37) were used only during development on a rented CPU machine to label mutants, which the policy allows. The server never calls them.
✓stateless per requestEach request is tokenized and classified on its own, with no gradients, cache, index or cross-request statistics (app.py
Each request is tokenized and classified on its own, with no gradients, cache, index or cross-request statistics (app.py). serve.sh runs a single worker.
✓actual inference uses reviewed weightsserve.sh sets MODEL_DIR=./model and runs uvicorn app:app. app.py loads its tokenizer and model from MODEL_DIR, which con
serve.sh sets MODEL_DIR=./model and runs uvicorn app:app. app.py loads its tokenizer and model from MODEL_DIR, which contains model/model.safetensors: a ModernBERT encoder with a 2-way classifier head, per the inventory. That is the only checkpoint and there is no alternate path. The trajectory shows /workspace/work/final from the GPU training run being copied into /workspace/output/model (trajectory#77). Only the tokenizer config files were later replaced with base-model copies (trajectory#87).
✓training data provenanceThe training data in all.jsonl (all2) is the deduplicated union of /task/public/validation.jsonl, labeled.jsonl and labe
The training data in all.jsonl (all2) is the deduplicated union of /task/public/validation.jsonl, labeled.jsonl and labeled2.jsonl (trajectory#64, trajectory#65). The labeled files hold mutants that mutate.py and mutate2.py built from the shipped validation attempts, labeled by the participant's own Lean v4.15.0 compiles (trajectory#37). data_manifest.md documents this. A search of the trajectory found no miniF2F, load_dataset or other dataset downloads. All of these sources are permitted derivatives of the shipped file.
✓non specialist initializationarchitecture.json declares answerdotai/ModernBERT-base at a pinned revision. train.py initializes AutoModelForSequenceCl
architecture.json declares answerdotai/ModernBERT-base at a pinned revision. train.py initializes AutoModelForSequenceClassification from that base with num_labels=2, and the log shows the newly initialized head (trajectory#67). The checkpoint inventory matches the ModernBERT architecture. This is a general pretrained encoder, not a specialist validity model.
✓harness credentials used only by the harnessSearches of the trajectory found no use of the harness API keys or base URLs, no model API calls from the participant's
Searches of the trajectory found no use of the harness API keys or base URLs, no model API calls from the participant's code, and no additional harness CLI sessions. The only credentials handled were Spin's S3 transfer session credentials (session.json) for spin s5cmd transfers, plus public Hugging Face downloads. Neither is a harness credential.
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 2 of 4.
- 1failed2h 16m into the runtook 7m 36s
failed startup: Server did not become healthy in 300s (last /health probe: RuntimeError: Submission HTTP request failed: ConnectionRefusedError: [Errno 111] Connection refused); end of its log: icorn.main() File "/tmp/deps/click/core.py", line 1631, in __call__ return self.main(*args,
3 gates
- ✓review prerequisites
- ✓no-Lean scan
- ✗startup · Server did not become healthy in 300s (last /health probe: RuntimeError: Submission HTTP request failed: ConnectionRefusedError: [Errno 111] Connection refused); end of its log: icorn.main() File "/tmp/deps/click/core.py", line 1631, in __call__ return self.main(*args, **kwargs) ^^^^^^^^^^^^^^^^^^^^^^^^^^ File "/tmp/deps/click/core.py", line 1552, in main rv = self.invoke(ctx) ^^^^^^^^^^^^^^^^ File "/tmp/deps/click/core.py", line 1415, in invoke return ctx.invoke(self.callback, **ctx.params) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ File "/tmp/deps/click/core.py", line 910, in invoke return callback(*args, **kwargs) ^^^^^^^^^^^^^^^^^^^^^^^^^ File "/tmp/deps/uvicorn/main.py", line 448, in main run( File "/tmp/deps/uvicorn/main.py", line 620, in run config.load_app() File "/tmp/deps/uvicorn/config.py", line 434, in load_app return import_from_string(self.app) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ File "/tmp/deps/uvicorn/importer.py", line 19, in import_from_string module = importlib.import_module(module_str) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ File "/usr/lib/python3.12/importlib/__init__.py", line 90, in import_module return _bootstrap._gcd_import(name[level:], package, level) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ File "<frozen importlib._bootstrap>", line 1387, in _gcd_import File "<frozen importlib._bootstrap>", line 1360, in _find_and_load File "<frozen importlib._bootstrap>", line 1331, in _find_and_load_unlocked File "<frozen importlib._bootstrap>", line 935, in _load_unlocked File "<frozen importlib._bootstrap_external>", line 995, in exec_module File "<frozen importlib._bootstrap>", line 488, in _call_with_frames_removed File "/submission/app.py", line 6, in <module> tok=AutoTokenizer.from_pretrained(MODEL) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ File "/opt/venv/lib/python3.12/site-package ...[clipped]
- 2passed2h 25m into the runtook 3m 46s
startup 9.9 s of 300 s; 2/2 gates passed
7 gates
- ✓review prerequisites
- ✓no-Lean scan
- ✓startup · GET /health answered 200 after 9.9 s
- ✓POST /check · {"id": "v00000", "valid": false}
- ✓batch deadline · 3540 distinct copies of the 526 public attempts at concurrency 64: 151.2 s plus 5.9 s for the first request, 22.5 attempts/s; grading allows 600 s for its 3540 held-out attempts
- ✓failed requests · 0 of 3540 failed, timed out or were rejected after retries; each scores as the wrong verdict
- ✓healthy after requests
The agent's last message before its session ended.
Submitted. Model: ModernBERT-base fine-tuned on the 526 provided attempts plus 3,638 Lean-labeled mutants (Lean v4.15.0/Mathlib v4.15.0 labeling on rented CPU; 2,978 deduplicated training rows after round 2, valid oversampled ×3, 12 epochs). Random-split eval macro F1 reached 0.9075 in train.log. Serving is pure model inference in app.py via serve.sh, with provenance in architecture.json and data_manifest.md. frontier selfcheck PASSED: startup 9.9s, 22.5 attempts/s (3540 in 157s vs 600s limit), 0% failed requests; session submitted at 2026-10-12 20:39 UTC.