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.