recursive_lean_prover

Prove a theorem in Lean by splitting it up. Each lemma is planned, proved in prose, split into child lemmas where it needs to be, and formalized in a git worktree of its own. Every lemma your comparator and a fresh reviewer accept is written to a Markdown wiki as it lands.

flowverse v0.1.2

In hmz, open /flow → Flowverses → official and install recursive_lean_prover and installs humanize1, which it calls. Or run the release without installing anything:

hmz exec -f 'git+https://github.com/humanfia/recursive-lean-prover-flow@v0.1.2#recursive_lean_prover' …

repository

humanfia/recursive-lean-prover-flow

release

v0.1.2 · commit a50a8b4

earlier

v0.1.1 · v0.1.0

needs

humanize1 >=0.1.1,<0.2.0

licence

Apache-2.0

Read from humanfia/flowverse when this site was built.

worker: claude · codex · kimimeant for codex in both roles

at the prompt

❯ $recursive_lean_prover prove the theorem stated in PROBLEM.md, in Submission.lean

hmz exec

hmz exec -f recursive_lean_prover \
    -a worker=codex/gpt-5.6-sol:max -a reviewer=codex/gpt-5.6-sol:max \
    -p lean_target=Submission.lean -p 'comparator_command=bash tools/check-with-comparator.sh' \
    -p budget.duration=72h "$(cat PROBLEM.md)"

recursive_lean_proversimulated

The whole run, at rest. Step through it with the buttons, or drag the bar.

One lemma of the proof. A lemma that needs splitting sends child lemmas a level down, each running this same line at once; an accepted lemma goes into the wiki and unlocks whatever waited on it.

The run, turn by turn

1. worker — one plan; a session opened for this turn; runs humanize1:gen-plan
2. worker — a proof in prose; a session opened for this turn; hands reviewer as words: the proof
3. reviewer — audits every step; a session opened for this turn; hands worker as words: valid
4. worker — splits it in lemmas; a session opened for this turn; hands worker, as builder as words: proved lemmas
5. worker, as builder — Lean, on a branch; a session opened for this turn; runs humanize1:rlcr; hands comparator in the tree: the candidate
6. comparator — comparator passes; no turn of a model; hands reviewer in the tree: the same candidate
7. reviewer — reruns it: accepted; a session opened for this turn; hands the finish as words: into the wiki

It ends when the root theorem is proved, or the budget runs out.

Before you run it

• A clean Lean git repository, with .humanize/ in its .gitignore: the flow keeps its state there, under the name humanize's own directory had before it was .hmz/. Run the flow at its root.
• A comparator: a script that checks a candidate and exits zero, printing comparator_success, only when every check has passed. It gets HUMANIZE_NODE_ID, HUMANIZE_NODE_STATEMENT, HUMANIZE_LEAN_FILES, HUMANIZE_RUN_DIR and HUMANIZE_WIKI_DIR in its environment:

#!/usr/bin/env bash
set -euo pipefail
lake env lean Submission.lean
./tools/project-comparator "$HUMANIZE_NODE_ID"
printf '%s\n' 'Your solution is okay!'

• A task file stating the exact theorem, the Lean file that may be edited, anything that must not be read or changed, and any rules for accepting a proof.

How each lemma goes

1. One plan, written once by humanize1:gen-plan and never rewritten.
2. A proof in prose, revised from the reviewer's first invalid step until it holds.
3. A split, where the lemma needs one: child lemmas with exact Lean statements and the order they depend on each other in. Each child goes through these same steps.
4. Lean, in a worktree of its own: humanize1:rlcr builds the formal proof on a named branch.
5. Acceptance: your comparator passes, then a fresh reviewer runs it again. The lemma goes into the wiki, and whatever was waiting on it can start.

Lemmas whose dependencies are proved run at the same time, up to max_parallel_children. The run prints its directory as it starts; watch the graph of lemmas grow in the DAG.md there.

Roles and params

Role	What it is	How it is filled
worker	agent, required	-a worker=…	Writes every plan, proof and Lean formalization. Must be claude, codex or kimi: rlcr's guards work through its permission requests.
reviewer	agent, required	-a reviewer=…	Checks every proof and candidate, and reruns the comparator itself.
workspace	environment, local	the directory you start in; no -e	Your Lean repository, with a git worktree of it for every lemma formalized.

Each agent role takes one -a role=CLI[@PROVIDER]/MODEL[:EFFORT]; several roles may share one -a, comma-separated. There is no -e to give: workspace is a local environment, the directory you start the run in, and an -e naming it is refused. See Command-line specs.

Every turn is a fresh session. Both roles may write across your home directory and use the web.

Every param has a default:

Param	Default
lean_target	blank	The .lean file the worker edits. Blank lets it work that out.
comparator_command	bash tools/check-with-comparator.sh	The comparator, run without a shell. May use {node_id}, {node_dir}, {run_dir}, {wiki_dir}, {lean_target} and {lean_files}.
comparator_success	Your solution is okay!	What a passing comparator prints.
comparator_timeout	21600	Seconds each comparator run may take.
max_depth	2	How deep lemmas may be split, 0 to 6. The theorem itself is depth 0.
max_children	4	Most child lemmas one lemma may split into, 2 to 12.
max_nodes	24	Most lemmas in the whole run; at least 3 when max_depth is not 0.
max_parallel_children	24	Most lemmas worked on at once.
natural_proof_attempts	3	Prose revisions per batch. Another batch follows while the proof still fails.
decomposition_attempts	2	Tries at a valid split.
rlcr_rounds	20	Rounds of rlcr per lemma.
plan_turn_timeout	3600	Seconds one planning turn may take; 0 for no limit.
plan_total_timeout	14400	Seconds one lemma's planning may take; 0 for no limit.
stop_on_child_failure	true	Hold a lemma back when a child it needs fails.
artifact_dir	.humanize/recursive-lean-prover	Plans, proofs, the graph of lemmas and logs. Must be under .humanize/.
wiki_dir	.humanize/math-wiki	The wiki of accepted lemmas. Must be under .humanize/.
node_attempts	2	Accepted for compatibility; it changes nothing.
plan_attempts	1	Fixed at 1: each lemma gets exactly one plan.

What ends it

• The theorem is proved, or refused, with the reason, which the next run starts from.
• The budget.
• A refused account, or a model the backend will not run. A turn that fails in a way a retry may fix is simply tried again.

Picking it up

Run the same line with --resume, in the same repository. It reuses the run, the lemmas already accepted, their worktrees and branches, the wiki, and the latest prose proof that was turned down. See Picking a run up.

See also

• humanize1: the phases it is built from
• A flow that calls a flow: how one flow runs another