Lean Formalization
Skill id:
lean-formalization
Generated from JSON Schema — do not edit by hand. Run bun run cat-harness/scripts/gen-schema-docs.ts.
Input
Input schema for the lean-formalization skill. Describes source material to be formalized in Lean 4.
| Field | Type | Required | Description |
|---|---|---|---|
sourceFile | string | yes | Path to the source material (LaTeX, markdown, or existing Lean file) to formalize. |
targetModule | string | yes | Lean module path for the output (e.g. ‘Qou.CategoryTheory.Functors’). |
proofStrategy | "tactic" | "term" | "mixed" | no | Preferred proof style. (default: "tactic") |
dependencies | array | no | Lean package dependencies (lake packages). |
Output
Output schema for the lean-formalization skill.
| Field | Type | Required | Description |
|---|---|---|---|
leanFiles | array | yes | |
buildStatus | "success" | "warnings" | "errors" | yes | |
diagnostics | array | no |
leanFiles[]
| Field | Type | Required | Description |
|---|---|---|---|
path | string | yes | |
module | string | yes | |
sorryCount | integer | no | min: 0 |
diagnostics[]
| Field | Type | Required | Description |
|---|---|---|---|
file | string | no | |
line | integer | no | |
severity | "error" | "warning" | "info" | no | |
message | string | no |