Formath

关于

Formath aims to streamline the process of formalizing mathematical content from TeX papers into Lean, leveraging LLMs and agents. It organizes extracted mathematical ideas into a consistent intermediate representation, facilitating step-by-step conversion into Lean code. The tool emphasizes minimal human intervention, easy resumption of work, fidelity to Lean's structure, source tracking, and a clear separation of stages from natural language to Lean.

主要功能

• Supports agent-driven workflows for automated and semi-automated proof generation
• Extracts and structures mathematical entities like concepts, definitions, and facts
• Generates Lean code stubs and artifacts, including LSP diagnostics integration
• 0 GitHub stars
• Manages project progress and tasks for formalization workflows
• Converts TeX documents to an intermediate Formath JSONL representation and Lean code

使用案例

• Managing the progress of large-scale mathematical formalization efforts
• Formalizing mathematical papers written in TeX into Lean projects
• Generating Lean proof stubs and integrating with Lean's LSP for verification
• Extracting structured mathematical entities from TeX for agent processing