Colloquia & Seminars

Title: From Markov processes to path integrals 

Joint Math/CMSA Geometry and Quantum Theory Seminar Speaker: Tomer Schlank Title: From Markov processes to path integrals Abstract: We will continue with Chapter 2 of the book and cover how we take the Markov process approach and Wick rotation to give a rigorous definition of path integrals.  

Title: CMSA Q&A Seminar: Denis Auroux, Harvard

CMSA Q&A Seminar Speaker: Denis Auroux, Harvard Title: What is Lagrangian Floer homology?  

Title: AI for the Working Mathematician

AI for the Working Mathematician Speaker: Harold Williams, USC Title: An Informal Introduction to Formal Proofs Abstract: In this talk we will give an introduction to Lean, a programming language adapted to expressing and verifying proofs. Lean and its flagship library, mathlib, have been the focus of a dedicated user community for about a decade, but their visibility has grown significantly in the last year. This is in large part because Lean makes validating large AI-generated proofs dramatically more practical: the human work is reduced from analyzing the logical correctness of an entire proof to analyzing the semantic correctness of a Lean statement. The main goal of the talk will be to build some example-based intuition for how...

Title: Geometry and Mathematical Physics Seminar

Geometry and Mathematical Physics Seminar Speaker: Tobias Ekholm, Uppsala  

Title: Painlevé VI: the search for canonical representations

Member Seminar Speaker: Aaron Landesman Title: Painlevé VI: the search for canonical representations Abstract: In 1902, Painlevé classified second order differential equations whose only movable singularities are poles, thereby obtaining the six Painlevé equations. Algebraic solutions to Painlevé's sixth equation correspond to canonical triples of 2 by 2 complex matrices. One can alternatively view these canonical triples of matrices either as canonical representations of fundamental groups of surfaces or as local systems on certain moduli spaces of curves. In this talk, based on joint work with Josh Lam and Daniel Litt, we will survey what is known about these canonical representations.

Title: Colloquium

Colloquium Speaker: Subhabrata Sen (Harvard)

Title: Geometry and Quantum Theory Seminar

Joint Math/CMSA Geometry and Quantum Theory Seminar  

Title: CMSA Q&A Seminar: Shaoyun Bai, MIT

CMSA Q&A Seminar Speaker: Shaoyun Bai, MIT Title: What is a virtual fundamental cycle? (ICM Series: On the work of John Pardon) Abstract: One of Pardon’s important contribution to symplectic topology is a new approach to constructing virtual fundamental cycles/chains for moduli spaces of pseudo-holomorphic maps. As a former PhD student of John, my own research has also been greatly influenced by his work on VFCs. I will try to explain some pieces of this framework and discuss how they are related to some of Pardon’s more recent work.    

Title: New Technologies in Mathematics Seminar

New Technologies in Mathematics Seminar Speaker: tba

Title: Geometry and Mathematical Physics Seminar

Geometry and Mathematical Physics Seminar Speaker: John Alexander Cruz Morales, Universidad Nacional de Colombia  

Title: Member Seminar

Member Seminar Speaker: Lorenzo Riva

Title: AI for the Working Mathematician

AI for the Working Mathematician Speaker: Jordan Ellenberg, University of Wisconsin-Madison Title: TBA

Title: Geometry and Quantum Theory Seminar

Joint Math/CMSA Geometry and Quantum Theory Seminar  

Title: Prove2Me: Formalizing Fermat Last Theorem and Beyond

New Technologies in Mathematics Seminar Speaker: Tianyi Peng, Decision, Risk, and Operations Division, Columbia Business School Title: Prove2Me: Formalizing Fermat Last Theorem and Beyond Abstract: Proof assistants such as Lean 4 promise the paradigm of formally verified mathematics, but large-scale formalization projects have faced major barriers to entry, including the need for expertise in formal verification (as well as the underlying mathematics) and the significant time required for writing formal proofs. AI coding agents have dramatically reduced these barriers; human users can now use natural language to prompt agents to write complex proofs in Lean. This opens up the intriguing possibility of internet-scale mathematical collaboration involving both humans and AI agents, where correctness is machine-checked.

Title: AI for the Working Mathematician

AI for the Working Mathematician Speaker: Lauren Williams, Harvard Title: First Proof Batch 3: Mathematicians putting AI to the test