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.