Enhancement of mathematical learning using the LEAN computer proof assistant
The proposed project aims to enhance students' proof-writing skills in mathematics through the use of the LEAN computer proof assistant. Developing rigorous mathematical reasoning and proof-writing abilities is crucial for students across STEM disciplines, yet traditional homework grading often fails to provide timely and detailed feedback to help students. The LEAN computer proof assistant offers an interactive environment where students can write proofs and receive instant feedback on the logical validity of each step. We will cover the basic mathematics required in science and engineering, which may seem intuitive, but writing down a formal and rigorous proof can be challenging. We will keep the entry cost low, so that students can learn mathematics through the LEAN language with minimal prior knowledge of LEAN. However, we encourage students with more experience to formalize mathematics that are of interest to them, and contribute their work to the LEAN mathematical library, thereby engaging them with the latest developments in the field of mathematical formalization.
