Project leader: Professor Colleen Robles
Project manager: Daniel Zhou
Team members: Huiyu Chen, Adam Kern, Justin Morrill, Letian Yang
The Linear Algebra Game is an innovative educational tool that teaches the Lean 4 proof assistant through the familiar context of linear algebra concepts. Rather than simply learning abstract mathematical theorems, students engage with an interactive game where they construct formal proofs step-by-step, building both their understanding of rigorous mathematical reasoning and proficiency in Lean 4's proof language. The game transforms traditional linear algebra topics—from vector spaces to linear transformations—into engaging puzzles that require students to think precisely about mathematical logic while mastering the syntax and techniques of modern theorem proving software.
This project implements a comprehensive formalization of undergraduate linear algebra in Lean 4, designed primarily as a pedagogical framework for teaching formal proof techniques rather than advancing the mathematical library. Using the lean4game infrastructure, we have created an interactive environment where students learn Lean 4's tactic language, type system, and proof strategies through the structured progression of linear algebra theorems from Axler's "Linear Algebra Done Right." The game's architecture includes custom educational tactics, carefully scaffolded proof exercises, and a dependency-aware blueprint system that visualizes the logical relationships between theorems, making it an effective tool for introducing mathematicians and computer scientists to the principles of mechanized mathematics and formal verification.
To get the final project report, one may visit the link to see how to play the game: