Methods · LeanGraph

Benchmark

Mathlib held-out. From every Mathlib module, we compute how many modules import it, directly or transitively, by parsing file headers. A module is eligible only if at most 20 modules depend on it and none of those is a tactic implementation. For a theorem from module M, the proof may not use any constant from M or from anything built on M, and the retriever never indexes them. Theorems whose statement itself mentions a constant from a banned module are dropped, because their definitions' unfolding lemmas would be banned too. Each statement is rendered from Lean's own signature and kept only if Lean confirms it is exactly the original theorem's type. Whole modules are assigned to a development split (prompt design) or the test split, never both; sampling round-robins across modules so no module contributes more than three theorems. Selection never looks at whether any prover can solve a theorem.

Authored. Theorems written for this project, each with a reference proof that passes the certifier. They measure how much held-out success depends on remembering Mathlib's own theorems.

Verification

A search-time check runs in a long-lived Lean REPL with Mathlib loaded. The verdict comes from a second, independent check: a fresh lean process compiles the proof as a file and a probe reports the axioms it depends on, every constant its proof term uses, and every declaration the file added, each line tagged with a random nonce generated after the proof was written. Proofs containing sorry, admit, axioms, native_decide, set_option, metaprogramming or top-level commands are rejected before compilation, and the certifier rejects them again independently if that filter is switched off (tested).

Agents

Every configuration is the same loop with parts switched on or off. Model draws are cached under a hash of the prompt and sample index, so two configurations that send the same prompt use the same draw: repair's first draft is the direct baseline's draft. The gateway's generation proved nearly deterministic for a given request, whatever the temperature, so the resampled drafts of Direct ×4 (samples 2–4) each send a fixed seed; a first, unseeded run, in which the four drafts were identical for 98 of 173 theorems, is kept as evidence.

Configurations

Template (no LLM)	A fixed list of automation tactics (simp, omega, linarith, nlinarith, positivity, aesop, grind, exact?, …) tried in order. No model.
Direct	One model draft, checked once.
Direct ×4	Four drafts: the Direct draft plus three resampled with fixed seeds (unseeded repeats were near-identical at this gateway). The equal-budget control for repair: same number of model calls, no feedback.
Repair	One draft, then up to three rounds in which the model sees Lean's exact error output.
Hybrid retrieval	One draft with eight lemmas retrieved from Mathlib (hybrid retriever) in the prompt.
Hybrid retrieval + repair	Retrieval plus up to three compiler-feedback repair rounds.
Full (plan + retrieval + repair)	A planning call (informal sketch plus a Lean `have` skeleton that Lean type-checks), then retrieval plus repair.
BM25 retrieval + repair	Retrieval + repair, with BM25 retrieval only.
Dense retrieval + repair	Retrieval + repair, with dense retrieval only.
Full − retrieval	The full agent without retrieved lemmas.
Full − compiler feedback	The full agent, but a failed round only says the proof failed; Lean's output is withheld.
Full − memory	The full agent, but each repair round shows only the latest attempt.
Full − skeleton	The full agent with an informal plan only, no Lean skeleton.
Direct (paraphrased prompt)	Direct with a paraphrased prompt (prompt-sensitivity check).
Repair (paraphrased prompt)	Repair with a paraphrased prompt (prompt-sensitivity check).

Task list build

{
  "counts": {
    "mathlib_heldout/dev/algebra": 5,
    "mathlib_heldout/dev/category_theory": 5,
    "mathlib_heldout/dev/inequalities": 5,
    "mathlib_heldout/dev/number_theory": 5,
    "mathlib_heldout/dev/probability": 5,
    "mathlib_heldout/dev/sets": 4,
    "mathlib_heldout/test/algebra": 20,
    "mathlib_heldout/test/category_theory": 20,
    "mathlib_heldout/test/functions": 6,
    "mathlib_heldout/test/inequalities": 20,
    "mathlib_heldout/test/number_theory": 20,
    "mathlib_heldout/test/probability": 20,
    "mathlib_heldout/test/sets": 15,
    "novel/test/algebra": 10,
    "novel/test/category_theory": 4,
    "novel/test/functions": 7,
    "novel/test/inequalities": 10,
    "novel/test/number_theory": 10,
    "novel/test/probability": 4,
    "novel/test/sets": 8
  },
  "difficulty": {
    "mathlib_heldout/easy": 50,
    "mathlib_heldout/hard": 50,
    "mathlib_heldout/medium": 50,
    "novel/easy": 22,
    "novel/hard": 7,
    "novel/medium": 24
  },
  "novel_authored": 53,
  "novel_certified": 53,
  "roundtrip_failures_skipped": 100
}

Environment

Generated from the lockfiles by a script, not typed by hand. Regenerate it whenever a pin changes.

Lean

Item	Value
Toolchain	`leanprover/lean4:v4.33.1`
`lean --version`	`Lean (version 4.33.1, arm64-apple-darwin24.6.0, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)`
Lean REPL	`leanprover-community/repl` at `5d5c49d13dfc0c1d2df43a27c3e56e02ad81b9c3`; its `lean-toolchain` is set to the pin above before building
Default heartbeat budget	200000 per theorem (`set_option maxHeartbeats 200000 in`)
Wall-clock backstop	60 s per REPL check, 600 s per certification

Lake manifest (`lean_env/lake-manifest.json`)

Package	Commit	Requested
`mathlib`	`0df444a360eaa60ab8c11dca51a86af692955474`	`v4.33.1`
`plausible`	`b7eb3304aeae834b12dda98993a37f6a41f6f0bb`	`main`
`LeanSearchClient`	`5f4d51b81cbd3f6b32b156bfad9056621a040404`	`main`
`importGraph`	`16f02aa7642864af59f1ff0e384a015994db9118`	`main`
`proofwidgets`	`4be2e3d5087eeb272cf5a8853b8f9dd025ef5957`	`main`
`aesop`	`3448c0bcc5ce01b2d1546e483ec3620e32df3d0e`	`master`
`Qq`	`92c15be17b7caf78c2ad767ec40f89052d908d81`	`master`
`batteries`	`4488d40d070b9700d4d5a6aa342f0d40c31b2a2d`	`main`
`Cli`	`6130a47896ce867c6a4a55373441e59e565bad0f`	`v4.33.0`

Python

Python 3.11 venv. Pinned packages (requirements.txt):

fastembed==0.8.0
httpx==0.28.1
matplotlib==3.11.1
numpy==2.4.6
onnxruntime==1.29.0
pandas==3.0.5
pytest==9.1.1
PyYAML==6.0.3
scipy==1.17.1

Machine used for the frozen results

Darwin 24.1.0 (arm64), 12 logical cores, 24 GB RAM. Each REPL worker holds Mathlib in memory (~4.7 GB RSS measured), so the default pool is 2 workers.

Model

Item	Value
Endpoint	OpenAI-compatible gateway at `api.gariyuuu.com/v1` (the owner's own)
Model id sent	`Yuu no Sekai` (the only model the gateway lists)
Upstream	The gateway's own docs (`gariyuuu-web/FEATURES.md`) name OpenRouter `qwen/qwen3-8b`; responses carry `"provider": "Alibaba"`. We did not verify the upstream independently.
Context limit reported by gateway	8192 tokens
Tiers	`/no_think` appended (reasoning off) is the default tier; `*_think` configs leave reasoning on
Sampling	temperature 0.6; every response cached under a content hash in `results/llm_cache/`

Benchmark

Verification

Agents

Configurations

Task list build

Environment

Environment

Lean

Lake manifest (lean_env/lake-manifest.json)

Python

Machine used for the frozen results

Model

Lake manifest (`lean_env/lake-manifest.json`)