Using Proof Burrower

Using Proof Burrower

Build

cargo build --release   # needs Rust stable (rust-toolchain.toml)

The binary is target/release/burrower.

Index a library

burrower index /path/to/HOL/Library --output idx.json

Walks .thy, .v and .lean files and stores lemma signatures.

Find a home for one goal

burrower find 'lemma foo: "a + b = b + (a::nat)"' --index idx.json --top 5

Ask the swarm

burrower swarm 'lemma foo: "a + b = b + (a::nat)"' --index idx.json --ledger burrow.jsonl

Each specialist scores its relevance, gives a reading in its own vocabulary, and proposes homes. The synthesis lists consensus homes and boundary objects.

Attempt proofs

Needs echidna and Isabelle on PATH (or --echidna /path/to/echidna).

burrower attempt 'lemma foo: "a + b = b + (a::nat)"' --ledger burrow.jsonl

Options: --timeout, --project-root (goals that import project theories), --sandbox none|bwrap|podman, and --oracle tools/julia-oracle.jl --oracle-descriptor d.a2ml for the optional tropical-types pre-proof oracle.

Read the ledger

burrower ledger recent --path burrow.jsonl
burrower ledger digest --path burrow.jsonl

A success recorded with a receipt came from echidna's structured result; a success recorded as a warrant came from an older echidna's text output. See ECHIDNA Contract.

Serve

burrower serve --socket /tmp/burrower.sock

Line-delimited JSON: {"cmd":"swarm"|"attempt"|"ledger"|"ping","args":{...}}.