Lean ai formalization
USE FOR: Formal verification of AI systems — agentic AI safety, alignment, high-stakes AI, evolving agents, neural network properties, and AI governance constraints. Use when formalizing safety envelopes, trust dynamics, multi-agent composition, AI act compliance, reward specifications, alignment properties, or any AI system property that must be formally verified. DO NOT USE FOR: AI methodology itself (use @ai-high-stakes-verifiable or @ai-agentic-evolving); security-specific formalisation (use @lean-security-formalization); knowledge formalisation (use @lean-knowledge-formalization). TRIGGERS: AI formalization, agentic safety, alignment proof, high-stakes AI, neural network property, AI governance.From its SKILL.md
npx -y skills add r-irbe/proof-skills --skill lean-ai-formalizationAssembled from the repository path, not quoted from the project. Check it against their README if it does not work.
One thing to look at
- 2 stars2 stars. Stars are a popularity signal and not a quality one, but at this level it is likely that nobody has read this closely except its author, and you would be relying on your own review.
SKILL.md
4.1 KB, 727 tokens by cl100k_base, as published. Nobody here has run it
Lean 4 AI Systems Formalization
Guide to formally verifying properties of AI systems, from safety envelopes to alignment guarantees.
Routing
- USE FOR: Formal verification of AI systems — agentic AI safety, alignment, high-stakes AI, evolving agents, neural network properties, and AI governance constraints. Use when formalizing safety envelopes, trust dynamics, multi-agent composition, AI act compliance, reward specifications, alignment properties, or any AI system property that must be formally verified.
- DO NOT USE FOR: AI methodology itself (use @ai-high-stakes-verifiable or @ai-agentic-evolving); security-specific formalisation (use @lean-security-formalization); knowledge formalisation (use @lean-knowledge-formalization).
- TRIGGERS: AI formalization, agentic safety, alignment proof, high-stakes AI, neural network property, AI governance.
Workflow
- Identify the AI property to formalise: safety, alignment, agentic invariant, or neural-network property.
- Pick the matching section of the body (verification framework, formal-property catalog, alignment-axiom set).
- Produce the Lean statement + proof skeleton; verify against the current Mathlib pin before delegating to
@lean-proof. - Hand off: to
@lean-proof-reviewonce the proof compiles, to@lean-enforcementfor the CI gate, to@lean-zettelkastenfor the pattern.
Recovery & STOP
- STOP if the property has not been formally stated — delegate to
@lean-specificationfirst. - STOP if Mathlib does not yet have the needed primitives — escalate to
@lean-research. - STOP if the AI system is agentic/emergent — delegate dynamics modelling to
@ai-agentic-evolvingfirst.
Handoffs
- Predecessors:
agent:gateway,skill:lean-research. - Successors:
skill:lean-proof-review,skill:lean-enforcement,skill:lean-zettelkasten,skill:lean-doc-feedback.
Detailed reference
Full content for lean-ai-formalization lives in
references/lean-ai-formalization-handbook.md.
Load that file when the skill is convened; the SKILL.md only carries
the dispatch contract and the parts index.
| Section | Topic |
|---|---|
| Part 1 | AI Safety Properties |
| Part 2 | Agentic AI |
| Part 4 | High-Stakes AI Verification |
| Part 5 | Neural Network Properties |
| Part 6 | Multi-Agent Composition |
| Part 7 | Commonsense and Causal Reasoning |
| Part 8 | Research Council Integration |
See also
../../references/lean-ai-formalization-handbook.md— Full handbook (extracted from this skill)../lean-proof-review/SKILL.md— Successor../lean-enforcement/SKILL.md— Successor../lean-zettelkasten/SKILL.md— Successor../lean-doc-feedback/SKILL.md— Successor
What ships with it
Read from the repository
Just SKILL.md. No reference files, no scripts.