Proof Burrower

Find the mathematical home of a proof goal.

Given a lemma you are stuck on, Proof Burrower searches theorem-prover libraries for the place where that goal already lives (or nearly lives), routes it through a small swarm of specialist "readers", and optionally attempts proofs through ECHIDNA, recording every attempt in an append-only ledger so the next run starts from what the last one learned.

ECHIDNA is the prover. Burrower is the librarian and the lab notebook.

Status: pre-alpha (v0.0.1). The Rust engine, CLI, ledger, socket service and WASM shim are implemented and tested; the CLI surface may still change. See docs/status/ROADMAP.adoc.

Table of Contents

• What it does
• Talking to ECHIDNA
• Quick start
• Layout
• Licence

What it does

Command	What it does
burrower index <root> --output idx.json	Walk a library tree (.thy, .v, .lean), extract lemma signatures, build an inverted index.
burrower find "<goal>" --index idx.json	Rank candidate homes for one goal (Jaccard over signature tokens).
burrower swarm "<goal>" --index idx.json [--ledger l.jsonl]	Route the goal through the specialists (Algebraist, Combinatorialist, Order-Theorist): each scores relevance, reads the goal in its own vocabulary, and returns homes; synthesis reports consensus homes and boundary objects.
burrower attempt "<goal>" --ledger l.jsonl [--echidna echidna]	Run every engaged specialist’s tactic playbook through echidna prove --prover Isabelle, and record each outcome in the ledger.
burrower ledger recent|by-specialist|anti-patterns|digest	Read the ledger back.
burrower serve --socket /tmp/burrower.sock	Expose swarm / attempt / ledger over a Unix socket (line-delimited JSON) for ECHIDNA and echidnabot.

Talking to ECHIDNA

burrower attempt invokes echidna prove. When the installed echidna supports --output json, Burrower reads the echidna.prove.result/1 object it prints (one JCS-canonical I-JSON line) and records a receipt: the prover, the axioms the proof rests on, and echidna’s version. With an older echidna that lacks the flag, Burrower falls back to the legacy text markers and records the success as a warrant (no receipt). The contract, detection rule and failure mapping are in docs/ECHIDNA-INTEGRATION.adoc.

Quick start

cargo build --release
./target/release/burrower index /path/to/HOL/Library --output idx.json
./target/release/burrower swarm 'lemma foo: "a + b = b + (a::nat)"' --index idx.json
# needs echidna (and Isabelle) on PATH:
./target/release/burrower attempt 'lemma foo: "a + b = b + (a::nat)"' --ledger burrow.jsonl

More: docs/QUICKSTART.adoc.

Layout

Path	Contents
crates/burrower-core	Engine: goal parsing, corpus index, ranking, specialists, attempts, the echidna contract, ledger, socket service, oracle bridge.
crates/burrower-cli	The burrower binary.
crates/burrower-wasm	C-ABI WASM shim for ECHIDNA’s typed-wasm oracle.
agents/*.007	Specialist definitions in the 007 agent DSL.
src/interface/	Idris2 ABI + Zig FFI layer (template scaffold; see docs/status/PROOF-STATUS.adoc for what is and is not proved).
docs/	Architecture, integration, design notes, status.
tests/e2e.sh	Live end-to-end check against real Isabelle via echidna.

Licence

Code: MPL-2.0. Documentation: CC-BY-SA-4.0. See LICENSE and LICENSES/.