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.