- Faculty mentor: Jarod Alper
- Graduate student mentors: Vasily Ilin, Leopold Mayer
- Student participants and contributors: Griffin Golias, Kevin Kuei, Brendan Murphy, Alex Scheffelin, Runchi Tan
- GitHub repository
Project
Developed our own library for ideals of commutative rings and formalized Hilbert's 1890 proof that ideals in polynomial rings are finitely generated.