Reap! A Friendly Tactic for Drafting Formal Proofs

With the release of our stepwise proving system Real‑Prover, we’re introducing reap, yet another lightweight Lean 4 tactic that helps you draft formal proofs one step at a time. reap wraps a premise‑selection service and an LLM into a minimal, composable interface so you can (a) get ranked, parse‑checked next‑move suggestions, (b) click to apply them in VS Code’s Infoview, and (c) extend the pipeline withyour own implementation.

TL;DR

• Three entry points:
  • reap — pick and apply a good next tactic step.
  • reap! — apply a step only if it solves the goal; otherwise fail.
  • reap? — list clickable suggestions (with proof‑state previews) in Infoview.
• Infoview widget: a “Try this” panel with colored status: 🎉/green = closes the goal; blue = valid step; gray = invalid.
• Clean internals: Requests (curl‑backed HTTP to manage POST and GET elegantly), OpenAIClient (Chat/Completions to offer familiar standard OpenAI-compatible experience), PremiseSelectionClient (caching + JSON), TacticGenerator (prompting + result filtering).

Installation

Add a dependency in your lakefile.lean or lakefile.toml:

require "reap" from git "https://github.com/frenzymath/reap.git"

Then import where you write proofs:

import Reap

Note. reap’s HTTP layer shells out to curl. Make sure curl is on your PATH.

Quick start

A minimal interactive session:

open Finset Set
example (s t : Finset ℕ) (h : s ⊆ t) (h' : t ⊆ s) : #s = #t := by
  -- Exploration panel with ranked, clickable suggestions
  reap?
  -- Or: try to advance one step automatically
  -- reap
  -- Or: apply only if it closes the goal
  -- reap!

Common patterns:

• Use reap? when you want transparency: it shows legal moves and a short consequence summary (goal preview).
• Use reap to nudge a stuck proof forward.
• Use reap! in small goals or teaching demos where closing the goal in one shot is reasonable.

Configuration

All runtime knobs live under the tacticgenerator.* options namespace so you can tweak them per‑file or per‑project without changing code. Typical settings:

-- LLM endpoint and credentials (OpenAI‑compatible)
set_option tacticgenerator.llm_endpoint "<Your LLM endpoint>"
set_option tacticgenerator.llm_api_key  "sk-…"
set_option tacticgenerator.model        "awesome-reaper"  -- or a local compatible model

-- Sampling / budget
set_option tacticgenerator.temperature  0.6
set_option tacticgenerator.num_samples  8
set_option tacticgenerator.max_tokens   256

-- Premise selection service
set_option tacticgenerator.ps_endpoint  "https://your-premise-service/query"
set_option tacticgenerator.num_premises 6

You can set these options globally, in a .lean file header, or interactively in Infoview. If you maintain an internal gateway (e.g., a local OpenAI‑compatible server), point llm_endpoint to it to keep traffic on‑prem.

Server Deployment

For now, our prover model can be pulled from huggingface, and deployed by any inference library. Premise-selection model can be pulled from huggingface, and can be deployed with code from github repo. We are also planning to provide a public-available service of this 2 components. Feel free to reach us if you like!

Prompt & result format (developer notes)

• OpenAI‑compatible requests. OpenAIClient sends chat requests of the form {model, messages=[{role="user", content=…}], n, temperature, max_tokens}.
• Lean‑side types. OpenAIMessage, OpenAIChatChoice/Response mirror the JSON schema and derive FromJson/ToJson where appropriate.
• Filtering. After parsing the LLM response, reap de‑duplicates and keeps only strings that parse as tactic, then runs the validation pass described above.

Extending reap

reap is intentionally small and modular. You can plug new components without changing the tactic surface:

• Premise selection. Implement your own PremiseSelectionClient.getResults : CoreM (Array PremiseSelectionResult) that hits any HTTP endpoint. The shipped client is a thin wrapper over Requests.post with a small in‑memory cache.
• Alternative LLMs. Point tacticgenerator.llm_endpoint/model at a local server (e.g., vLLM or similar) if you don’t want to depend on external APIs.
• Prompt shaping. Fork the prompt in TacticGenerator to prefer certain tactic families (e.g., simp/linarith) or to ask for structured outputs.
• UI. The Infoview widget is just a few dozen lines of React; it’s easy to customize the rendering or add keyboard navigation.

Roadmap

• Better formatting of reap? previews (pretty‑printer improvements).
• Local retrieval helpers for offline demos.
• Deployment-side optimization to ensure deterministic generation.

Acknowledgements

reap stands on the shoulders of excellent open tooling and prior work, including LeanCopilot, and LLMLean. Thanks to the Lean Zulip community for ideas and feedback.

Get involved

• Repo & issues: https://github.com/frenzymath/reap
• Zulip thread: (to be posted alongside this blog)

If you try reap in a course, a workshop, or a codebase, we’d love to hear how it goes—and what you’d like it to do next.