I am a senior mathematics student at Cornell University.
I'm currently exploring Morse Theory under the supervision of Professor Xin Zhou and working with Professor Xiaodong Cao as a book assistant for "Differential Geometry and Applications" by Richard Hamilton, Monique Chyba, and Xiaodong Cao.
I am developing a formal proof library for differential geometry using the Lean 4 programming language. The goal of this project is to build a self-contained foundational library for geometric analysis.
Currently formalized theorems include: