DuoTactic — a Lean 4 proof-search harness

32.8 % of miniF2F test, 34.8 % of miniF2F valid, 45 s per problem, every accepted proof re-compiled by the Lean kernel. DuoTactic ships with a 39.58 M-parameter tactic model as an optional candidate generator; the measured end-to-end contribution of that model to those two numbers is 0 of the 165 solved problems (see Provenance of the score).

中文说明: README.zh.md · Usage guide (EN) · 使用说明（中文）

What DuoTactic is

One sentence: a proof-search harness for Lean 4 that closes a goal by searching the compositions of a fixed table of public automation tactics and only believes what the kernel re-compiles.

Concretely, one by-tactic-shaped system with four moving parts:

1. A fixed 16-entry automation table (--force-set v2: rfl, ring, omega, simp_all, linarith, trivial, nlinarith, aesop, simp, norm_num, simp_all ; ring, simp_all ; norm_num, simp_all ; omega, simp_all ; linarith, gcongr, field_simp ; ring), injected at every frontier node of every depth — so the search also composes them (simp_all then ring), not just tries them once.
2. Depth-batched best-first search over the resulting candidate pool (k=16, beam 4, depth 6, 45 s wall clock per problem, 30 s per round).
3. Batched kernel verification: all candidates of a round go into a few .lean files, one lean --json call each, and diagnostics are attributed back to candidates by line number.
4. A confirmed verdict or nothing: a problem counts as solved only if the accepted proof re-compiles standalone — exit code 0, no error, no sorry, and (audited) axiom dependencies ⊆ {propext, Classical.choice, Quot.sound}.

An optional 40M tactic model can feed extra candidates into the same pool (it competes with the table on equal terms); it is not required, and --no-model switches it off completely.

What DuoTactic is not — read this before comparing it to other tools

In the literature a hammer is defined as premise selection + translation to an external automatic theorem prover + reconstruction of a verified proof (Sledgehammer, Magnushammer, LeanHammer). DuoTactic does none of those three: there is no premise retrieval, no translation to an external ATP, and no reconstruction from an external proof trace. Its whole search happens inside Lean's kernel. Structurally it is closer to aesop (white-box best-first proof search over a rule set) with a hand-fixed rule set, a per-problem budget and a verification back end.

	premise selection	external ATP	reconstruction	composition search	batched kernel verification
Sledgehammer / Magnushammer	✓	✓	✓	partial	—
LeanHammer	✓	✓	✓	aesop	—
DuoTactic	✗	✗	✗	✓	✓

Results

End-to-end miniF2F (search configuration in docs/USAGE.md). One run per problem, one attempt — pass@1 with a search harness, not pass@k sampling:

Setting	Problems	Passed	Wall
DuoTactic (model in the pool)	valid, all 244	85/244 = 34.8 %	2.3 h
DuoTactic (model in the pool)	test, all 244	80/244 = 32.8 %	2.5 h
DuoTactic (model in the pool)	valid, first 89	30/89 = 33.7 %	51.7 min
model variant e6 instead of stage3-e3	valid, first 89	30/89 = 33.7 %	59.8 min
DuoTactic, --no-model (table only)	valid, first 10	2/10 = 20 %	3.3 min
(older, weaker protocol: depth-1 injection, v1 table)	valid, all 244	8/244 = 3.3 %	—

Segments of the full valid split: 0-89 → 33.7 %, 89-178 → 40.4 %, 178-244 → 28.8 %. Proof length: 78 of the 85 solutions are a single tactic (2 / 2 / 3 solutions at depths 2 / 3 / 4). Test split segments: 38.2 % / 27.0 % / 33.3 %, 76 of the 80 solutions are a single tactic. All 165 accepted proofs are confirmed.

Provenance of the score (read before quoting it)

The numbers above are harness numbers produced by items 1–4 of What DuoTactic is, with the 40M model merely adding candidates to the same pool. Classifying every accepted proof by where its winning tactic came from:

Final tactic of the accepted proof	valid (85 solved)	test (80 solved)
the injected automation table, single step	78	76
the injected table, multi-step chain	7	4
a tactic proposed by the 40M model	0	0

78/244 (valid) and 76/244 (test) are the initial goal closed by one injected tactic at depth 1 — for those problems no model is in the loop at all. Disabling the model changes nothing: --no-model on valid problems 0-9 returns 2/10 — the same problems, at the same depths, with the same proof terms — in 3.3 min instead of 6.5 min (the model's candidates roughly double the wall clock and add no solution).

Honest one-liner: a search over public Lean automation tactics, with kernel-checked verification, solves 32.8 % of miniF2F test and 34.8 % of valid at 45 s per problem; the attached 40M tactic model supplies 0 of those solutions. Do not present these figures as a neural tactic-generation result, and do not compare them with model-only pass@1 numbers from the literature (those have no automation table; DuoTactic with the table removed would score 0).

Reproducing both sides of the ablation:

# the reported numbers (model in the pool)
python code/eval_minif2f.py --split test  --n 244 --k 16 --beam 4 --depth 6 \
    --budget 45 --round-budget 30 --force --force-set v2 --force-depth 99 \
    --lean-parallel 10 --verify-chunk 64 --narrow-imports \
    --ckpt checkpoints/stage3-e3 --tag test244

# the same harness with the model switched off
python code/eval_minif2f.py --split valid --n 244 --k 16 --beam 4 --depth 6 \
    --budget 45 --round-budget 30 --force --force-set v2 --force-depth 99 \
    --lean-parallel 10 --verify-chunk 64 --narrow-imports --no-model \
    --ckpt checkpoints/stage3-e3 --tag nomodel244

How strong is it? Published baselines

System	Class	miniF2F	Notes
Isabelle Sledgehammer	bare hammer	20.9 %	the baseline every hammer paper reports
Isabelle Magnushammer	hammer + premise selection	34.0 %	+13 points from premise selection alone
Lean tidy (Lean 3)	built-in automation	23.8 %	on LeanDojo-random, not miniF2F — indicative only
DuoTactic	automation + composition search	32.8 % test / 34.8 % valid	45 s per problem
Lean GPT-f (2021)	neural + search	24.6 % test pass@1	10 min per problem, no automation table
ReProver / LeanDojo (2023)	neural + retrieval + search	25.9 % test / 26.5 % valid
DeepSeek-Prover-V1.5-RL (2024)	neural + MCTS	50.0–50.7 % test	pass@32/64
InternLM2.5-StepProver 7B	neural	65.9 % test / 69.6 % valid
BFS-Prover / V2 (2025)	neural + tree search	72.95 % / 95.08 % test

Read that cautiously: the neural rows use per-problem budgets and sample counts far above our 45 s / single attempt, and the Isabelle rows are a different proof assistant. The defensible claim is narrow: DuoTactic sits at the level of a premise-selecting hammer and ~1.6× above the bare-hammer baseline, while being cheap (45 s/problem) and fully kernel-verified. It is not competitive with neural provers, and it is not meant to be.

Independent support for the design choice: on miniF2F-test, DeepSeek-Prover-V1.5-RL improves from 42/244 to 55/244 when a fixed schedule of 15 tactic skeletons is placed in the prompt, while doubling the sampling budget (k=32 → k=64) finds zero additional proofs (Inference-Time Diversity in RL-Trained Lean Provers, 2026). A fixed tactic skeleton schedule — i.e. exactly what DuoTactic's table is — is a stronger inference-time lever than more sampling, even for a 7B RL model.

The tactic model (leanoar-schemec-40m) — an optional component

A from-scratch 39.58 M-parameter decoder-only transformer that reads a Lean 4 proof state (trace_state-style text, including the ⊢ goal line) and writes one tactic. Trainable and runnable on a single 8 GB consumer GPU (RTX 4060 Laptop: 4.83 GiB VRAM, 36 k tok/s, 35.7 min for one epoch over 317 k samples). Its dev metric is real; its end-to-end contribution is not (0/165).

pip install -r code/requirements.txt        # torch, tokenizers, numpy, safetensors

python code/verify_package.py               # verify this package against its own documented numbers
python code/generate.py                     # real dev example -> top-5 tactics
python code/generate.py --ckpt checkpoints/stage3-e3 --k 8
python code/eval_dev.py --all --compare     # recompute the dev metric for both variants

verify_package.py checks four things and prints PASS/FAIL: the parameter count, the dev protocol (1024 fixed rows) against metrics.json, inference wiring, and the checksums. Real, unmodified output of python code/generate.py on the packaged dev example #0:

--- real dev example #0 (row 0 of the packaged dev split) ---
--- state ---
T : Theory L
h : M ≅[L] N
⊢ M ⊨ T ↔ N ⊨ T
--- top-5 tactics (device=cuda, ckpt=checkpoints/e6) ---
  -0.512  rw [IsUnit.iff_eq_bot] exact h.symm simp only [IsUnit.iff_eq_true
  -1.044  simp only [IsUnit.iff_eq, h.eq_iff, not_and_or, not_and_or]
  -0.475  refine ⟨fun h ↦ ?_, fun h ↦ h.trans h.symm⟩ exact h.symm exact h.symm exact h
  -0.105  constructor rw [IsUnit.iff_eq_bot] exact h.symm simp [h.symm]
  -0.694  exact ⟨fun h => h.trans h.symm, fun h => h.symm ▸ h.symm⟩ exact h.symm
--- the tactic mathlib actually used here (reference) ---
  rw [Theory.model_iff_subset_completeTheory, Theory.model_iff_subset_completeTheory,
  h.completeTheory_eq]

That is what the model really produces: structurally plausible openers (refine ⟨fun h ↦ ?_, …⟩), sensible context references (h.symm), and some concatenated garbage. Nothing matches the reference tactic — which is exactly why verification is not optional.

Dev, first-token protocol (first 1024 FORWARD rows of the packaged dev split; logits at mask_start-1 predicting the token at mask_start). This is the only protocol comparable across models — the trainer's logged dev numbers use a length-bucketed reshuffle and must not be compared.

Variant	top-1	top-5	CE
checkpoints/e6	0.3076	0.7090	2.5494
checkpoints/stage3-e3	0.2891	0.7246	2.4971
trivial baseline (most frequent first token)	0.2171	0.6079	—

Architecture

Component	Spec	Parameters
Backbone	decoder-only, 8 layers, d_model 640, 10 heads (head_dim 64), RoPE, RMSNorm, dropout 0.1	—
Attention projections	Q/K/V/O = 4 × 640×640, no bias	13,107,200
SwiGLU FFN	d_ff 1536 (gate/up/down)	23,592,960
Token/output embedding	4096 × 640, tied with the output projection	2,621,440
Policy head	low-rank 640 → 128 → tied embedding	163,840
Value head	MLP 640→128→32→3, observed under stop-grad only (experimentally negative, see below)	86,275
RMSNorm ×17, misc	—	10,880
Total	context 768, vocab 4096	39,582,595

The tied embedding plus a low-rank policy head keeps the model under 40 M, which is what makes the whole data → train → search loop fit on one 8 GB card. generate() uses no KV cache (prefix generation ≈ 12.4 ms/token), but that is ~8 % of wall clock; Lean compilation is 91 %.

Training data

A. LeanDojo/Mathlib traces (base split). Of 87,766 mathlib declarations, 41,944 carry tactic traces → 169,530 (state, tactic) pairs; 15 % REPAIR augmentation (a proof step replaced by its own prefix state) + exact de-duplication by token payload → 188,501 training samples.

B. Self-built replay mining ("E6", new data). 45,822 declarations had no trace; sampling showed 37 % of them are := by proofs — only the states were missing. Method: wrap every prefix of every source proof in its own probe declaration and read the state back from Lean's unsolved goals error message; tactic boundaries are detected automatically by state change. Result: 8,536 files / 88,418 declarations / 401,523 probes → 136,258 pairs in 83 minutes with 6-way parallelism, and 0 pairs containing sorry/admit. Merged and de-duplicated against the base split: 317,492 train / 6,165 dev samples (steps_v2, context 768, covering 99.4 % of proof steps).

Note the distribution shift: the mined data mostly adds proof-structure tactics (refine share 0.55 % → 7.77 %, convert! 0 → 1 %, multi-line tactics 9.1 % → 22.4 %) while goal-closing tactics drop (47.6 % → 27.6 %).

Variant	Init	Data	Recipe	Wall
stage3-e3	low-lr fine-tune from an LM-pretrained checkpoint	188,501	lr 2e-5, 1 epoch tactic-only	14.5 min
e6	from scratch	317,492	1.5-epoch cap, early stop (best step 5000)	35.7 min

What we measured about this component (four findings)

1. The two variants solve exactly the same 30 problems (first 89) at exactly the same depths — zero gained, zero lost. Raising dev top-1 from 0.2891 to 0.3076 (+1.85 points) bought nothing end-to-end and cost 16 % wall clock. This is the third independent time a model-side improvement failed to transfer to pass@1.
2. Candidate-level reality: only 7.9 % of proposals type-check; 56.6 % of states yield at least one type-checking candidate, but only 6.3 % yield one that closes the goal. The bottleneck is closing, not proposing.
3. The value head is not usable: AUC 0.5201 vs 0.7475 for the policy's own confidence; reranking with it hit valid candidates 7.0 % of the time vs 19.6 % for plain top-1. Do not use it to rerank.
4. The tail of the split is not a collapse: without injection the last 66 problems score 1.5 % (first 89: 3.4 %), with injection they score 28.8 %. What lifted them was automation coverage, not any change in how hard the problems are.

Known limitations of the model

1. Emits one tactic at a time; long proofs need external search to chain candidates.
2. Whole-tactic greedy exact match 0/200 — treat the output as candidates, never as answers.
3. Repetition degeneration happens (ring ring ring ring, h₂ h₂ h₂ h₂); search-side de-dup and Lean verification contain it.
4. Hard-bound to the v1 id space: always pair with tokenizer_v1.json. The project's other tokenizer (tokenizer.json) has an extra <|premises|> and shifts every content id by one; pairing it with these weights produces gibberish and a bogus CE.
5. Context 768 is baked in. Longer states are truncated to head 60 % + tail 40 % (the goal line is last). The prompt also reserves 4 special tokens plus the generation window: the harness budgets ctx − 4 − max_new_tokens state tokens.
6. Model-side gains do not move pass@1 (see above). For a higher score, invest in the verifier/search side — that is where every measured gain came from.

Known limitations of the harness

1. No premise selection: DuoTactic cannot invent a library lemma name, so problems whose proof needs a specific mathlib lemma it does not try are out of reach — that is the main reason the score stops at ~33 %.
2. Lean/mathlib version sensitive: collected and evaluated on Lean 4.35.0-rc2 + a mathlib4 snapshot (Sept 2026). Two miniF2F problems do not compile on mathlib master at all (mathd_numbertheory_711, imosl_2007_algebra_p6).
3. Fixed budget: 45 s per problem and depth 6 cap the search; the ablation shows throwing more time at it was not where the gains were.
4. Narrow imports: with --narrow-imports each problem's header is replaced by #min_imports + Mathlib.Tactic (3.41 s → 1.74 s per lean --json call, 1.98× end-to-end on already-solved problems). Any candidate failing with "unknown identifier/tactic" is automatically re-checked with the full import, so narrowing cannot lose a proof (verified 85/85).

Files

Path	What it is
code/eval_minif2f.py	DuoTactic itself — the end-to-end harness that produced every pass rate in this card.
code/leanoar/search.py	depth-batched best-first search, frontier management, budgets, whitelist, confirmed verdict.
code/leanoar/lean_batch.py	batched lean --json verification, confirm(), narrow-import computation.
code/leanoar/model.py, code/leanoar/data.py	the 39.58 M model and its dataset/tokenizer plumbing.
checkpoints/e6/	model weights: lit_model.pth + model.safetensors + training_meta.json. Highest dev top-1 (0.3076).
checkpoints/stage3-e3/	model weights, end-to-end best variant (same architecture and size). Identical pass@1 to e6, 16 % faster.
config.json	Authoritative architecture, context length, special-token ids, prompt template, weight roles.
metrics.json	Every measured number, each with the protocol it was measured under.
tokenizer_v1.json	Must be paired — v1 id space (8 specials, ids 0–7).
special_tokens_v1.json	The 8 special token ids.
first_token_whitelist.json	64 most frequent first tokens of the training split (97.6 % coverage).
examples/dev_sample.jsonl	16 real dev states + the tactic mathlib actually used on them.
data/dev/	The dev protocol arrays (1024 fixed rows + build_meta.json) so anyone can recompute the headline metric.
data/minif2f/	miniF2F valid/test records + their .lean files, as used by the harness.
data/whitelist/	Small seed files from which the search code derives the first-token whitelist (instead of shipping 479 MB of training arrays).
code/common.py, generate.py, eval_dev.py, verify_package.py	loading / sampling / metric reproduction / one-shot package verification.
docs/USAGE.md / docs/USAGE.zh.md	Usage guide: standalone inference, metric reproduction, end-to-end search with Lean.
SHA256SUMS	Checksums of every file in the package.
LICENSE / NOTICE	Apache-2.0 text + upstream provenance (mathlib4, LeanDojo, miniF2F).

Loading the model needs three things: config.json + a weight file (lit_model.pth or model.safetensors) + tokenizer_v1.json. code/generate.py is the minimal correct example — copy from it. Running the harness needs Lean + mathlib as well (next section).

End-to-end search (needs Lean + mathlib)

code/eval_minif2f.py ships the harness that produced the numbers above, including the exported automation-tactic table (--force-set v2). It needs a working Lean 4.35.0-rc2 toolchain and a mathlib4 checkout with a prebuilt .lake cache (≈10 GB); point the package at them with:

export LEANOAR_LEAN_BIN=/path/to/lean-4.35.0-rc2-linux/bin/lean
export LEANOAR_MATHLIB=/path/to/mathlib4
python code/eval_minif2f.py --n 89 --ckpt checkpoints/stage3-e3      # reproduce 30/89

Full setup, the exact search configuration, expected runtimes and troubleshooting: docs/USAGE.md. Measured cost: 2 125 lean --json calls in 3.3 h on the valid split, 2 921 in 2.5 h on test with narrow imports (3.1 s per call).

Provenance and license

• Weights, tokenizer and data are derived from mathlib4 (Apache-2.0) and LeanDojo traces (MIT). miniF2F (data/minif2f/) is MIT. Released under Apache-2.0, consistent with upstream — keep the provenance note if you redistribute, and cite mathlib4 and LeanDojo: they supplied all of the supervision. What this project adds is the pipeline, the search harness and the 40 M model.
• Training/inference environment: Python 3.13, torch 2.14 (cu130), WSL2 Ubuntu 24.04, single RTX 4060 Laptop (8 GB).
• Research artifact: no guarantee that any generated tactic is correct. Only the Lean kernel decides that — which is why every number here is a re-compilation, not a similarity score.