Title

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.

Location

ECL 114

Start Date

3-25-2023 9:30 AM

Presentation Format

Oral Only

Group Project

No

COinS
 
Mar 25th, 9:30 AM

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.