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 |