proof-theory skill

by parcadei·parcadei/Continuous-Claude-v3·3.9k stars·MIT

Problem-solving strategies for proof theory in mathematical logic

A100/100content scan

Is the proof-theory skill safe?

Clean: nothing in its files matched our rules. We read 1 file in the folder on 2026-09-28.

No findings.

Install the proof-theory skill

A skill is a folder. Copy it into your agent's skills folder and the agent loads it when the task matches its description.

git clone --depth 1 https://github.com/parcadei/Continuous-Claude-v3.git /tmp/Continuous-Claude-v3
mkdir -p ~/.claude/skills
cp -r /tmp/Continuous-Claude-v3/.claude/skills/math/mathematical-logic/proof-theory ~/.claude/skills/proof-theory

available in every project

In the Claude apps, zip the folder and upload it from the Skills settings. The folder on GitHub

The instructions your agent would load

SKILL.md as published, without the frontmatter. Read it on GitHub

Proof Theory

When to Use

Use this skill when working on proof-theory problems in mathematical logic.

Decision Tree

Proof Strategy Selection

Direct proof: assume premises, derive conclusion
Proof by contradiction: assume negation, derive false
Proof by cases: split on disjunction
Induction: base case + inductive step

Structural Induction

Define well-founded ordering on structures
Base: prove for minimal elements
Step: assume for smaller, prove for current
z3solve.py prove "inductionprinciple"

Cut Elimination

Gentzen's Hauptsatz: cuts can be eliminated
Subformula property: only subformulas appear
Useful for proof normalization

Completeness/Soundness Check

Soundness: if provable then valid
Completeness: if valid then provable
z3solve.py prove "soundnesstheorem"

Proof Verification

Check each step follows from rules
Verify dependencies are satisfied
mathscratchpad.py verify "proofsteps"

Tool Commands

Z3InductionBase

uv run python -m runtime.harness scripts/cc_math/z3_solve.py prove "P(0)"

Z3InductionStep

uv run python -m runtime.harness scripts/cc_math/z3_solve.py prove "ForAll([n], Implies(P(n), P(n+1)))"

Z3_Soundness

uv run python -m runtime.harness scripts/cc_math/z3_solve.py prove "Implies(derivable(phi), valid(phi))"

Math_Verify

uv run python -m runtime.harness scripts/cc_math/math_scratchpad.py verify "proof_structure"

Cognitive Tools Reference

See .claude/skills/math-mode/SKILL.md for full tool documentation.

More skills from parcadei/Continuous-Claude-v3

Aagent-context-isolationAgent Context Isolation
Aagent-orchestrationAgent Orchestration Rules
Aagentic-workflowAgentic Workflow Pattern
Aagentica-claude-proxyGuide for integrating Agentica SDK with Claude Code CLI proxy
Aagentica-infrastructureReference guide for Agentica multi-agent infrastructure APIs
Aagentica-promptsWrite reliable prompts for Agentica/REPL agents that avoid LLM instruction ambiguity
Aagentica-sdkBuild Python agents with Agentica SDK - @agentic decorator, spawn(), persistence, MCP integration
Aagentica-serverAgentica server + Claude proxy setup - architecture, startup sequence, debugging
Aagentica-spawnSpawn Agentica multi-agent patterns
Aanalytic-functionsProblem-solving strategies for analytic functions in complex analysis
Aast-grep-findAST-based code search and refactoring via ast-grep MCP
Aasync-repl-protocolAsync REPL Protocol

All agent skills → · MCP servers