formalize_tex
Converts TeX documents into Lean code via Formath JSONL, generating entities.jsonl and lean/src/<module>.lean files in sibling directories. Streamlines mathematical formalization workflows.
Instructions
End-to-end minimal pipeline: TeX -> Formath JSONL -> Lean stub module.
Writes to sibling directories beside the TeX's tex/ folder: formath/entities.jsonl and lean/src/<module>.lean.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| module_name | No | Main | |
| tex_path | Yes |
Input Schema (JSON Schema)
{
"properties": {
"module_name": {
"default": "Main",
"title": "Module Name",
"type": "string"
},
"tex_path": {
"title": "Tex Path",
"type": "string"
}
},
"required": [
"tex_path"
],
"title": "formalize_texArguments",
"type": "object"
}