gpd-formalize-rung
OfficialGenerate Lean 4 formalization scaffolds for stable theorem rungs
AuthorUnified-Field-Theory-Research
Version1.0.0
Installs0
System Documentation
What problem does it solve?
This Skill helps automate the creation of Lean 4 formalization scaffolds for stable theorem rungs, making the process of translating theorems into Lean-compatible formalizations more efficient.
Core Features & Use Cases
- Automated Scaffold Creation: Generates Lean 4 formalization scaffolds for theorems, with explicit hypotheses, parameters, and proof obligations.
- Customizable: Allows for specifying a theorem rung by name or obligation to create the appropriate formalization.
- Use Case: Suppose you have a complex theorem rung with numerous assumptions and proof obligations. Using this Skill, you can generate a formalization scaffold that outlines the structure of the Lean proof, streamlining the process and making it easier to get started.
Quick Start
Use the gpd-formalize-rung skill to generate a Lean formalization scaffold for a stable theorem rung with the following command:
cargo run --quiet --manifest-path rust/cclab_accel/Cargo.toml --bin cclab -- skill formalize-rung --project-dir . --obligation OBL-000
Dependency Matrix
Required Modules
Lean
Components
scripts
💻 Claude Code Installation
Recommended: Let Claude install automatically. Simply copy and paste the text below to Claude Code.
Please help me install this Skill: Name: gpd-formalize-rung Download link: https://github.com/Unified-Field-Theory-Research/finite-capacity-causal-geometry/archive/main.zip#gpd-formalize-rung Please download this .zip file, extract it, and install it in the .claude/skills/ directory.
Agent Skills Search Helper
Install a tiny helper to your Agent, search and equip skill from 620,000+ vetted skills library on demand.