scillm Tools

LLM completions and formal proofs via scillm (per SCILLM_PAVED_PATH_CONTRACT.md).

Tools

Tool	Purpose
batch.py	Batch LLM completions via parallel_acompletions
prove.py	Lean4 theorem proving via certainly

---

batch.py - LLM Completions

Quick Start

# Single completion
python .agents/skills/scillm/batch.py single "What is 2+2?"

# Single with JSON response
python .agents/skills/scillm/batch.py single "Return {answer: number}" --json

# Batch from file
python .agents/skills/scillm/batch.py batch --input prompts.jsonl --json

Commands

Single completion:

python .agents/skills/scillm/batch.py single "Your prompt" [--json] [--model MODEL]

Batch completions:

python .agents/skills/scillm/batch.py batch \
  --input prompts.jsonl \
  --output results.jsonl \
  --json \
  --concurrency 6

Input/Output Format

Input JSONL (one per line):

{"prompt": "Summarize..."}
{"prompt": "Translate..."}

Output JSONL:

{"index": 0, "content": "...", "ok": true}
{"index": 1, "error": "timeout", "status": 408}

Environment Variables

Variable	Required
CHUTES_API_BASE	Yes
CHUTES_API_KEY	Yes
CHUTES_MODEL_ID	Yes

---

prove.py - Lean4 Theorem Proving

Quick Start

# Prove a claim
python .agents/skills/scillm/prove.py "Prove that n + 0 = n"

# With tactic hints
python .agents/skills/scillm/prove.py "Prove n < n + 1" --tactics omega

# Check availability
python .agents/skills/scillm/prove.py --check

Commands

Prove a claim:

python .agents/skills/scillm/prove.py "Your claim" [--tactics simp,omega] [--timeout 120]

Check if ready:

python .agents/skills/scillm/prove.py --check

Output Format

Success:

{
  "ok": true,
  "lean4_code": "theorem add_zero (n : ℕ) : n + 0 = n := by simp",
  "compile_ms": 7406
}

Failure:

{
  "ok": false,
  "diagnosis": "mathematically false",
  "suggestion": "Change to 'Prove that 2 + 2 = 4'"
}

Tactic Hints

Tactic	Use for
simp	Identities, simplification
omega	Integer arithmetic
ring	Polynomial algebra
linarith	Linear inequalities

Prerequisites

1. lean_runner container running
2. OPENROUTER_API_KEY set
3. scillm[certainly] installed

---

Importable API (For Other Skills)

The quick_completion function can be imported by sibling skills:

# Add scillm to path (for sibling skills)
import sys
from pathlib import Path
sys.path.insert(0, str(Path(__file__).parent.parent / "scillm"))

from batch import quick_completion

# Simple completion
result = quick_completion("What is 2+2?")

# With JSON mode
result = quick_completion("Extract {name, age}", json_mode=True)

# With system prompt
result = quick_completion(
    prompt="Translate to French: Hello",
    system="You are a translator",
    temperature=0.3,
)

Parameters:

Param	Type	Default	Description
prompt	str	required	User prompt
model	str	env var	Model ID
json_mode	bool	False	Request JSON response
max_tokens	int	1024	Max tokens
temperature	float	0.2	Sampling temperature
timeout	int	30	Request timeout (s)
system	str	None	System prompt

---

Python API (Direct scillm)

For more control, use scillm directly:

# Single completion (for one-off calls)
from scillm import acompletion

resp = await acompletion(model=..., messages=[...], api_base=..., api_key=...)

# Batch completions (for parallel processing)
from scillm import parallel_acompletions

reqs = [{"model": MODEL, "messages": [...]}]
results = await parallel_acompletions(reqs, api_base=..., api_key=...)

# Lean4 proofs
from scillm.integrations.certainly import prove_requirement

result = await prove_requirement("Prove n + 0 = n", tactics=["simp"])

See SCILLM_PAVED_PATH_CONTRACT.md for full reference.