SketchRefine

Official open-source implementation of the ICML 2026 paper "Editable Proof Sketch for Automated Theorem Proving".

SketchRefine is a multi-stage pipeline that builds, verifies, and iteratively refines editable proof sketches in Lean 4. It coordinates large language models, a theorem search service, and a Lean verifier to solve formal mathematics problems such as those in MiniF2F.

Installation

Requires Python 3.9+.

pip install -r requirements.txt

You also need access to the following external services:

• A reasoning LLM endpoint (e.g. DeepSeek-compatible API).

• A prover LLM endpoint (OpenAI-compatible /v1 API).

• A Lean 4 verifier service. SketchRefine uses kimina-client to talk to a Kimina Lean server. Set up the server by following project-numina/kimina-lean-server, then point KIMINA_URL at it.

• A theorem search service. SketchRefine uses lean-explore as the retrieval backend. Install lean-explore and download its local data following that repository's instructions, then start the HTTP wrapper shipped with this project:

  python src/lean_explore_server.py --host 127.0.0.1 --port 8210

  Point QUERY_URL at the resulting endpoint (e.g. http://127.0.0.1:8210).

Configuration

Copy .env.example to .env and fill in the endpoints and API key:

cp .env.example .env

Variable	Description
ARK_API_KEY	API key for the token-limited reasoning LLM.
REASONER_URL	Base URL of the reasoning LLM endpoint.
REASONER_MODEL	Model name for the reasoner.
QUERY_URL	URL of the theorem search service.
PROVER_URL	URL of the prover LLM (OpenAI-compatible).
KIMINA_URL	URL of the Lean 4 verifier service.

Pipeline behavior (which stages run, retry counts, prompts, default header, etc.) is configured per benchmark in config/<benchmark>.yaml. See config/minif2f.yaml for the full schema.

Usage

Run the full MiniF2F benchmark with default paths:

python src/main.py

Common options:

python src/main.py \
  --data    data/minif2f.jsonl \
  --config  config/minif2f.yaml \
  --work-dir work/minif2f \
  --output  results/minif2f_results.json \
  --token-limit 2000000 \
  --limit 10

Arguments:

• --data Path to a JSONL benchmark file (each line has name and lean4_code).
• --config YAML configuration describing pipeline stages.
• --work-dir Per-problem working directory (logs, intermediate sketches).
• --output Aggregated results JSON file.
• --token-limit Token budget per problem for the reasoning LLM.
• --limit / --skip Slice the problem list for partial runs.

A summary JSON is written to --output and detailed per-problem logs are saved under --work-dir/<problem_name>/logs/.

Dataset

The MiniF2F benchmark file data/minif2f.jsonl can be downloaded from the Goedel-Prover-V2 repository, specifically dataset/minif2f.jsonl.