Project leader: Professor Colleen Robles
Project managers: Stavan Jain, Ricardo Prado Cunha, Anoushka Sinha
Team members: Will Harris, Clara Henne, William Ho, Adam Kern, Dominic King, Arim Lim, Justin Morrill
A mathematical proof is a logical explanation that establishes why a mathematical idea is true. These proofs are traditionally done using natural language and intuition, meaning they rely on the reader's understanding and cannot be easily checked by a computer. However, formal proofs use precise rules and syntax, allowing every step to be verified by a computer, ensuring they are more rigorous. To create and verify these formal proofs, mathematicians use proof assistants, special software tools designed to help develop and check mathematical proofs. One such tool is Lean 4, an open-source software that allows users to write formal arguments in a special programming language. Lean is particularly powerful because it not only checks the proofs but also helps guide users in constructing them. In this project, we used Lean to create an interactive problem set for students learning abstract algebra. Over six weeks, we completed four sections of this teaching aid, aiming to provide more insight into mathematical proofs and Lean. We hope future teams will continue building on our work, expanding the problem set further.
The final product of this project was the creation of “AlgebraInLean” (AIL), an interactive problem set that takes users through an advanced course in Lean through the lens of abstract algebra. The ultimate goal of “AlgebraInLean” is to introduce students to formalization and Lean 4 while also assisting in the process of writing rigorous proofs in group theory. Lean, along with many other theorem provers, leverages the Curry-Howard correspondence that establishes a link between logic and computation and allows mathematical proofs to be written as functional programs. Beginning with introductions to logic-based reasoning in Lean, the set takes users through various topics in group theory. Akin to Kevin Buzzard’s “Formalizing Mathematics” course at the Imperial College London, AIL includes chapters on group axioms, homomorphisms, and subgroups, each separated into problem sheets. These problem sheets include both the formalization of mathematical structures and exercises on proving related theorems. We defined group theory axioms outside of Lean’s Mathlib (Mathlib is a comprehensive mathematical library in the Lean theorem prover, designed to support a wide range of mathematical concepts, proofs, and computations) to provide a better learning experience for the user, including learning about Lean type theory while also using it as a teaching supplement for algebra. Also included in AIL is the Lean Blueprint, which provides a dependency graph of lemmas and definitions, a top-down view of formalization progress, and a bottom-up view of individualized nodes. While this problem set presents an extensive introduction to the formalization of algebra and group theory mathematics, there is much left for future contributions. We hope that others will add to the problem set in the future, including examples related to quotient groups, group actions, Sylow theorems, ring theory, and much more.
Link to algebra-in-lean (our final product)