tasks_autogen_from_entities
Generate tasks for entities without existing tasks to streamline mathematical formalization workflows in Formath MCP. Supports project scaffolding and entity management for Lean code conversion.
Instructions
Create open tasks for entities of given kind that do not already have tasks.
Default kind is 'fact' (lemmas). Returns number of tasks created.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| kind | No | fact | |
| project_root | Yes |