Embedded Files
In the 2026 Fall semester, the seminars will be held both online and in-person (CU216). Online talks are usually on Thursdays starting at 4:30 PM, and in-person talks will be on Mondays at 4:30 PM.
Organizers: Huai-Dong Cao, Andrew Harder, Ao Sun, Xiaofeng Sun.
If you are interested in participating in the seminar, please email Ao (aos223 at lehigh dot edu).
Monday 8/31/26 (In-person, CU 216, 4:30 PM)
Speaker: Yipeng Wang (Princeton)
Title: The Positive Mass Theorem in Arbitrary Dimensions
Abstract: We present an inductive scheme for proving the positive mass theorem in arbitrary dimensions, extending the Schoen–Yau argument from dimensions at most 7 to the general case. This is a joint work with Simon Brendle.
Monday 9/7/26 (In-person, CU 216, 4:30 PM)
Speaker: Xiaofeng Sun (Lehigh)
Title: Stability, Moment Maps and Hermitian-Yang-Mills Iterations
Abstract: Canonical metrics often arise as zeros of moment maps, while stability is encoded by the asymptotic slopes of Kempf–Ness functions. After recalling this principle in Kähler–Einstein geometry, GIT, and the Donaldson–Uhlenbeck–Yau theorem, I will introduce a shifted Hermitian–Yang–Mills iteration on a stable bundle and explain its monotonicity, a priori estimates, and exponential convergence to a Hermitian–Einstein metric. I will then outline a heat-flow and moment-weight proof of the Wang–Yang–Yau threshold theorem, showing that either the flow remains bounded and converges, or it produces a destabilizing saturated quotient. Finally, I will interpret the twisted equation as an extended moment-map equation, with the modified Donaldson functional playing the role of its Kempf–Ness function.
Monday 9/14/26 (In-person, CU 216, 4:30 PM)
Speaker: Yuan Liao (UCSD)
Title: (Auto-)formalizing Hamilton's Three-Manifold Theorem in Lean
Abstract: With recent advances in language models, it has become increasingly realistic to ask whether large parts of the existing mathematical literature can be formalized automatically.
In this talk, I will discuss joint work with Bennett Chow and Ziyang Qin on a Lean formalization of Hamilton’s three-manifold theorem. Rather than focusing on the details of Hamilton’s Ricci-flow argument, I will use the project as a case study in the workflow of large-scale autoformalization. I will first give a brief introduction to Lean, and then discuss where the real difficulties arise: choosing faithful definitions and theorem interfaces, decomposing a long proof into manageable dependencies, dealing with mathematical infrastructure that is absent from existing libraries, coordinating many local formalization tasks, and auditing the final development for both logical correctness and mathematical meaning.
A central question is which of these difficulties are intrinsic to a particular theorem and which represent one-time infrastructure costs that can be reused in later projects. I will discuss this distinction in the context of geometric analysis and compare our experience with recent large-scale formalization efforts, including Fermat’s Last Theorem and work surrounding the complex-structure problem for the six-sphere. The broader goal is to understand what a scalable pipeline for formalizing existing mathematics might look like, and what role mathematicians should play as more of the low-level formalization process becomes automated.
Monday 9/21/26 (In-person, CU 216, 4:30 PM)
Speaker: The Hoan Nguyen (UChicago)
Title: Min-max barrier and minimal foliations on the torus
Abstract: Aubry–Mather theory concerns minimizing orbits of convex Hamiltonian systems. Moser, Bangert, and Auer developed a higher-dimensional analogue for area-minimizing hypersurfaces. In this talk, I will describe this theory on a Riemannian torus. After lifting to the universal cover, each minimizing hypersurface carries an asymptotic invariant, called its homological direction, and hypersurfaces with a common direction organize into laminations. I will discuss recent work in which Almgren–Pitts min–max theory is used to characterize when such a lamination is a foliation. I will also explain how, for generic metrics, a gap in the lamination contains a complete embedded minimal hypersurface that is not area-minimizing.
Monday 10/19/26 (In-person, CU 216, 4:30 PM)
Speaker: John Loftin (Rutgers-Newark)
Title: TBD
Abstract: TBD
Monday 11/23/26 (In-person, CU 216, 4:30 PM)
Speaker: Christopher Kuo (Max Planck Institute for Mathematics)
Title: TBD
Abstract: TBD
Page updated
Google Sites
Report abuse