🧮 Introducing MathForm: An Open-Source Framework, Dataset, and Model for Mathematical Autoformalization

Summary

Introducing MathForm, an open-source framework, dataset, and model for mathematical autoformalization with Lean 4. Formalizing mathematics makes mathematical knowledge machine-checkable, but it is more than translating statements into code. A model must map each concept onto… (source truncated).