Zichen Wang, Wanli Ma, Zhenyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen
M2F is a framework that automates the formalization of entire mathematical textbooks into Lean code, achieving high proof success rates and significantly reducing the time needed compared to manual efforts.
The M2F framework is designed to convert entire mathematical textbooks into a format that computers can understand and verify, specifically using the Lean programming language. This process, called formalization, ensures that the mathematical content is accurate and can be checked by a computer. M2F automates this task, which traditionally takes experts months or years, completing it in just a few weeks. The framework was successfully used on textbooks about real and convex analysis, achieving a high rate of correctly formalized proofs.
