Prepare proof-pilot for crates.io: kernel-arbitrated LLM proof completion for Lean 4

crates/proof-pilot/Cargo.toml

@@ -3,7 +3,14 @@ name = "proof-pilot"
 version.workspace = true
 edition.workspace = true
 license.workspace = true
-description = "LLM-driven Lean proof completion loop via Claude CLI"
+description = "Kernel-arbitrated LLM proof completion for Lean 4, with anti-cheat and deterministic replay"
+repository = "https://github.com/LucidSamuel/scribe"
+homepage = "https://github.com/LucidSamuel/scribe/tree/main/crates/proof-pilot"
+documentation = "https://docs.rs/proof-pilot"
+readme = "README.md"
+keywords = ["lean", "theorem-proving", "llm", "formal-verification", "agent"]
+categories = ["development-tools", "mathematics", "science"]
+exclude = ["*.log"]
 
 [dependencies]
 serde = { version = "1", features = ["derive"] }

crates/proof-pilot/README.md

@@ -0,0 +1,69 @@
+# proof-pilot
+
+**A kernel-arbitrated LLM proof-completion loop for Lean 4, with anti-cheat and
+deterministic replay.**
+
+Point it at a Lean file with a `sorry` and an LLM backend. The loop edits the
+proof body, compiles the exact target file with `lake build`, feeds the errors
+(or structured LSP goal states) back to the model, and repeats until the **Lean
+kernel** accepts or the budget runs out. The model writes the proof; the kernel
+decides.
+
+```sh
+proof-pilot MyProject/Theorem.lean --lake-dir MyProject --max-iters 10
+```
+
+## Why trust the output
+
+- **The kernel is the oracle.** Success is `lake build` exiting clean on the
+  exact target file — never the model's claim of success.
+- **Anti-cheat.** The patcher structurally cannot modify the theorem statement:
+  everything up to `:= by` comes from the file, the model only fills the body,
+  and the splice is bounded by the next top-level command. A token-aware scan
+  (comment- and string-skipping) rejects `sorry`, `axiom`, and `native_decide`
+  in anything that would be spliced.
+- **Deterministic replay.** Every session produces a journal (optionally saved
+  as versioned JSON) recording each iteration — prompt, response, patch, build
+  output, and under best-of-n every candidate plus which one was accepted.
+  `--replay transcript.json` re-applies a session without calling any LLM, and
+  refuses on Lean-toolchain or Mathlib-revision mismatch unless you pass
+  `--allow-toolchain-mismatch`.
+- **Best-of-n sampling, soundness-free.** `--samples-per-iter K` fires K
+  attempts per iteration and lets the kernel filter: candidates are hash-
+  deduplicated, tried shortest-first, and the first to build wins. A wrong
+  candidate costs a build, never a false acceptance.
+
+## Backends
+
+`claude` (Claude CLI, default) · `anthropic` (Messages API) · `openai` ·
+any OpenAI-compatible endpoint (`openai-compat`, vLLM, ollama, hosted provers)
+via `--backend`, `--model`, `--api-key`, `--base-url`.
+
+## Feedback modes
+
+Default is raw `lake build` output. `--lsp` switches to structured Lean
+language-server feedback — goal states, hypotheses, tactic probes, and lemma
+search — via a bundled Python bridge over
+[`leanclient`](https://pypi.org/project/leanclient/). Final verification always
+uses `lake build` regardless of mode.
+
+## Extras
+
+- `--notes NOTES.md` — a human-readable debugging report mapping common Lean
+  error shapes to concrete guidance (embedders can attach their own
+  worked-example citations via `notes::NotesStyle`).
+- `--save-transcript session.json` — versioned JSON transcript with toolchain
+  and Mathlib-revision pinning.
+
+## Provenance
+
+Extracted from [scribe](https://github.com/LucidSamuel/scribe), where this loop
+proves soundness theorems for zero-knowledge circuit gadgets — and runs
+*adversarially* (proving negations to hunt counterexamples), which works
+unchanged because refutations answer to the same kernel. The loop itself is
+domain-agnostic: it needs a Lake project and a theorem, not any particular
+mathematics.
+
+## License
+
+MIT

crates/proof-pilot/examples/prove_sum_comm.rs

@@ -0,0 +1,50 @@
+//! Non-ZK example: complete an ordinary Mathlib-flavoured proof.
+//!
+//! Demonstrates that proof-pilot is domain-agnostic — the target here is a
+//! plain arithmetic lemma, not a circuit-soundness theorem. Requires:
+//! - a Lake project directory (pass as argv[1]) whose `lakefile` can build
+//!   files in its root, with Mathlib available if your theorem needs it;
+//! - the `claude` CLI on PATH (or edit `make_backend` below).
+//!
+//! ```sh
+//! cargo run -p proof-pilot --example prove_sum_comm -- path/to/lake-project
+//! ```
+
+use proof_pilot::backend::make_backend;
+use proof_pilot::session::{self, SessionConfig, SessionResult};
+
+const SCAFFOLD: &str = r#"import Mathlib.Tactic.Ring
+
+/-- An ordinary lemma with a `sorry` for the loop to fill. -/
+theorem sum_sq_comm (a b : ℕ) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
+  sorry
+"#;
+
+fn main() {
+    let lake_dir = std::env::args()
+        .nth(1)
+        .expect("usage: prove_sum_comm <lake-project-dir>");
+    let lean_file = format!("{lake_dir}/ProofPilotExample.lean");
+    std::fs::write(&lean_file, SCAFFOLD).expect("write scaffold");
+
+    let backend = make_backend("claude", None, None, None).expect("backend");
+    let config = SessionConfig {
+        lean_file: lean_file.clone(),
+        lake_dir,
+        max_iterations: 5,
+        system_prompt: None,
+        transcript: None,
+        use_lsp: false,
+        samples_per_iter: 1,
+    };
+
+    match session::run(&config, backend.as_ref()).0 {
+        SessionResult::Proven { iterations } => {
+            println!("kernel accepted after {iterations} iteration(s): {lean_file}")
+        }
+        SessionResult::Exhausted { iterations, .. } => {
+            println!("no proof in {iterations} iteration(s)")
+        }
+        SessionResult::Failed(msg) => eprintln!("error: {msg}"),
+    }
+}