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.”<\/p>\n\n\n\n
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<\/a> to try it.<\/p>\n\n\n\n Project leader<\/strong><\/p>\n\n\n\n Gavin Dooley (Notre Dame, Class of 2024)<\/p>\n\n\n\n Contributors<\/strong><\/p>\n\n\n\n Adrian Dooley (Chesterton High School, Class of 2024)<\/p>\n\n\n\n Xiaotong “Dawson” Yang (Notre Dame, Class of 2023)<\/p>\n\n\n\n Jiachen “Jenna” Zhao (Notre Dame, Class of 2024)<\/p>\n\n\n\n Faculty Sponsor<\/strong><\/p>\n\n\n\n David Galvin<\/a> (Notre Dame)<\/p>\n\n\n\nTeam<\/h2>\n\n\n\n
Contact<\/h2>\n\n\n\n