Northwestern Undergraduate Lean Lab

Through the Northwestern Undergraduate Lean Lab, I formalize mathematics in the Lean proof assistant. As a contributor to DeepMind’s Formal Conjectures project, I formalized number-theoretic conjecture statements and their supporting definitions in Lean. I am also developing Mathlib formalizations in multivariable calculus, including partial derivatives and Hessian matrices.