Will (Ziang) Li

About

I am a senior at Cornell majoring in Mathematics with a minor in Computer Science. My research interests lie in hyperbolic geometry, complex dynamics, Teichmüller theory, and differential geometry. Also, I have a side interest in AI for math, specifically autoformalization in Lean 4 (see my current project below).

Reading Project

I was introduced to the field of hyperbolic geometry and geometric topology by Prof. Benjamin Dozier. Currently, I am studying McMullen's Riemann Surfaces, Dynamics, and Geometry supervised by Prof. Yusheng Luo.

You can find my reading reports here: 

• Hyperbolic Manifolds, Tessellations, and Fundamental Domains (Fall 2025)

• Sullivan's Dictionary and Teichmüller Theory (Spring 2026)

Lean 4 Formalization

I am developing a Lean 4 library formalizing important results in complex dynamics, hyperbolic geometry, and Teichmüller theory, including No Wandering Domains Theorem, Uniformization Theorem, and Nielsen–Thurston Classification. Currently, I have successfully formalized:

• Schwarz–Pick Inequality

• Montel–Carathéodory Theorem

• Equivalence between the geometric and analytic definitions of quasiconformal mapping

• Measurable Riemann Mapping Theorem

• No Wandering Domains Theorem