proof-assistant
npx machina-cli add skill a5c-ai/babysitter/proof-assistant --openclawFiles (1)
SKILL.md
1.6 KB
Proof Assistant Skill
Purpose
Assist in constructing formal correctness proofs for algorithms using standard proof techniques.
Capabilities
- Proof structure templates (induction, contradiction, etc.)
- Step-by-step proof guidance
- Termination argument generation
- Proof review and validation
- Identify proof gaps
Target Processes
- correctness-proof-testing
- algorithm-implementation
Proof Techniques
Mathematical Induction
- Base case identification
- Inductive hypothesis formulation
- Inductive step construction
Proof by Contradiction
- Assumption negation
- Logical derivation
- Contradiction identification
Loop Invariant Proofs
- Invariant specification
- Three-part proof (init, maintenance, termination)
Structural Induction
- For recursive data structures
- Base case (leaf/empty)
- Inductive case (composite)
Input Schema
{
"type": "object",
"properties": {
"algorithm": { "type": "string" },
"code": { "type": "string" },
"proofType": {
"type": "string",
"enum": ["induction", "contradiction", "invariant", "structural"]
},
"claim": { "type": "string" },
"partialProof": { "type": "string" }
},
"required": ["algorithm", "claim"]
}
Output Schema
{
"type": "object",
"properties": {
"success": { "type": "boolean" },
"proof": { "type": "string" },
"structure": { "type": "array" },
"gaps": { "type": "array" },
"suggestions": { "type": "array" }
},
"required": ["success"]
}
Source
git clone https://github.com/a5c-ai/babysitter/blob/main/plugins/babysitter/skills/babysit/process/specializations/algorithms-optimization/skills/proof-assistant/SKILL.mdView on GitHub Overview
Proof Assistant helps you craft formal correctness proofs for algorithms using standard techniques like induction, contradiction, loop invariants, and structural induction. It offers templates, step-by-step guidance, termination arguments, and proof review to uncover gaps in your reasoning.
How This Skill Works
You provide the algorithm, a clear claim, and optional code or proofType. The tool offers proof structure templates (induction, contradiction, invariant, structural), guides you through base cases, inductive steps, and invariant maintenance, and generates termination arguments while highlighting any gaps for review.
When to Use It
- When you need to certify the correctness of a new algorithm before or alongside implementation
- When proving termination for recursive or loop-based algorithms
- When establishing loop invariants to reason about iterative processes
- When validating proofs for recursive data structures via structural induction
- When reviewing and filling gaps in existing correctness arguments
Quick Start
- Step 1: Provide the algorithm and the exact correctness claim, plus any optional code
- Step 2: Choose a proofType (induction, contradiction, invariant, or structural) and supply it
- Step 3: Use the templates to draft base/inductive steps or invariants, then review and refine to fill gaps
Best Practices
- Clearly state the algorithm and the exact correctness claim you intend to prove
- Choose the appropriate proof technique (induction, contradiction, invariant, structural) based on the problem
- Break proofs into clear base cases, induction or maintenance steps, and termination arguments
- Define precise invariants and recursion cases; annotate assumptions explicitly
- Test proofs against potential counterexamples and solicit feedback to identify gaps
Example Use Cases
- Proving binary search correctly returns an index of the target in a sorted array
- Proving termination and correctness of the Euclidean algorithm for gcd
- Proving the recursive factorial function computes n! via mathematical induction
- Proving that a loop invariant maintains correct prefix sums during iteration
- Proving that a tree-summing function yields the total of node values using structural induction
Frequently Asked Questions
Add this skill to your agents
