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.

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/.