Welcome to the Lean-Equipped Math Problem Generator, an ongoing project managed by Gavin Dooley. The goal of this project is to form a collection of web tools that generate proof-based math problems. While this project does not directly use the Lean proof assistant, it expresses problems and solutions in the language of Lean. Specifically, a problem is a “type” (expressed in Lean’s language) and a valid solution is a “term” of the given type. Currently, one mode of the problem generator is supported: “Universal Algebra.”
Universal Algebra
This mode generates problems regarding varieties (in the sense of universal algebra). Each problem concerns a specific (possibly many-sorted) variety (i.e., a collection of sets, equipped with some functions, constants, and equational laws). The goal of each problem is to derive another equational law from those given. Click here to try it.
Team
Project leader
Gavin Dooley (Notre Dame, Class of 2024)
Contributors
Adrian Dooley (Chesterton High School, Class of 2024)
Xiaotong “Dawson” Yang (Notre Dame, Class of 2023)
Jiachen “Jenna” Zhao (Notre Dame, Class of 2024)
Faculty Sponsor
David Galvin (Notre Dame)
Contact
To share questions, comments, suggestions, or ideas, email gdooley2@nd.edu.