Formalizing mathematics in LEAN

• Main Author: Liu, Yufei
• Other Authors: Gary Royden Watson Greaves
• Format: Final Year Project
• Language: English
• Published: Nanyang Technological University 2024
• Subjects: Mathematical Sciences; Mathematics formalization; LEAN4
• Online Access: https://hdl.handle.net/10356/175451
• Institution: Nanyang Technological University

This final year project is a journey into the realm of mathematics formalization, exploring the depths and boundaries of what it means to translate mathematical concepts into the precise programming language of LEAN4. LEAN4, a state-of-the-art theorem proving language, together with its official mathematical library mathlib, offers the capability to rigorously define and prove mathematical theorems. The focus of this project is to gain a deeper understanding of mathematical formalization and to demonstrate its application in advancing mathematical discourse. Formalizing matrix determinant lemma (MDL) was identified as a research gap during this exploration, as it had not yet been formalized in mathlib, providing a case study for applying the learned formalization techniques. This report outlines the methodology adopted, and the formalization process, highlighting the gradual learning curve with LEAN4, active engagement with the LEAN community, and the contributions made to the mathlib. A notable achievement of this project is the integration of the matrix determinant lemma into the official mathlib, enhancing the library’s functionality and demonstrating the practicality of LEAN4 in handling complex mathematical proofs. Furthermore, the development of HTML documentation provides an interactive platform to present this project, enhancing the engagement and comprehension of mathematics formalization.