Formalization of Elementary Row Operations Using LEAN
School Name
South Carolina Governor's School for Science and Mathematics
Grade Level
12th Grade
Presentation Topic
Mathematics
Presentation Type
Mentored
Abstract
LEAN is a programming language that helps write mathematical proofs by using mathlib, an open-source library with countless theorems and lemmas. LEAN is used to formalize proofs, allowing them to be more easily verified and understood by both computers and humans. The goal of the research was to add elementary row operations of matrices to mathlib using LEAN to allow for other mathematicians to build upon our work. By contributing to mathlib, these new theorems and lemmas reduce the amount of work required by future mathematicians, who can instead work on expanding boundaries instead of proving what has already been done. We first had to learn as much of the LEAN programming language using resources provided by Dr. Kevin Buzzard's Xena project as possible. The next step was to begin formalizing lemmas for elementary row operations using lemmas and theorems already in mathlib. We were able to create lemmas for each of the row operations on 2x2 and 3x3 matrices but were unsuccessful in generalizing the lemmas to any NxN matrix. In conclusion, even though what was accomplished may seem small, it is an excellent first step in proving many more complex theorems and lemmas related to matrices using LEAN, such as Gauss-Jordan elimination.
Recommended Citation
Sabin, Aidan, "Formalization of Elementary Row Operations Using LEAN" (2023). South Carolina Junior Academy of Science. 96.
https://scholarexchange.furman.edu/scjas/2023/all/96
Location
ECL 114
Start Date
3-25-2023 9:30 AM
Presentation Format
Oral Only
Group Project
No
Formalization of Elementary Row Operations Using LEAN
ECL 114
LEAN is a programming language that helps write mathematical proofs by using mathlib, an open-source library with countless theorems and lemmas. LEAN is used to formalize proofs, allowing them to be more easily verified and understood by both computers and humans. The goal of the research was to add elementary row operations of matrices to mathlib using LEAN to allow for other mathematicians to build upon our work. By contributing to mathlib, these new theorems and lemmas reduce the amount of work required by future mathematicians, who can instead work on expanding boundaries instead of proving what has already been done. We first had to learn as much of the LEAN programming language using resources provided by Dr. Kevin Buzzard's Xena project as possible. The next step was to begin formalizing lemmas for elementary row operations using lemmas and theorems already in mathlib. We were able to create lemmas for each of the row operations on 2x2 and 3x3 matrices but were unsuccessful in generalizing the lemmas to any NxN matrix. In conclusion, even though what was accomplished may seem small, it is an excellent first step in proving many more complex theorems and lemmas related to matrices using LEAN, such as Gauss-Jordan elimination.
