Date/Time : 25 Apr 2025 14:00
Venue : S17 #04-04 (SR3)
Speaker : Xu Tianyi, Peking University (BICMR)

This talk explores the latest developments and emerging trends in the application of AI to mathematics, focusing on leveraging generative models for writing formalized mathematical proofs. We will introduce the idea of formalizing mathematics using proof assistants—computer programs designed to verify the correctness of mathematical proofs. We will then compare various approaches to formalization, highlighting the unique advantages of using large language models (LLMs) for this task. Additionally, we will address key challenges that naturally arise in this process and present our strategies for overcoming them.

Add to calendar :

Date/Time : 14 Mar 2025 11:00
Venue : S17 #04-04 (SR3)
Speaker : Wang Yutong, National University of Singapore

In the previous sections, we have introduced some recent LLM tools in Lean 4, especially the ones for auto-formalization and auto-proving. In this lecture, I will show you the basic concepts and techniques behind these tools, and how you can use them to improve your efficiency in both formal and informal research. I will also try to introduce to you some recent progress in the field of LLM reasoning in mathematics.

Zoom link: https://nus-sg.zoom.us/j/84932999912?pwd=tSka7Th1z2McUW3zhjquuUQ7hcLfab.1
Zoom ID: 849 3299 9912
Pwd: 475364

Add to calendar :

Date/Time : 07 Mar 2025 11:00
Venue : S17 #04-04 (SR3)
Speaker : Wang Yutong, National University of Singapore

In this lecture, we will continue our unfinished discussion on structures and typical proof logic. We will resume our journey to introduce more advanced techniques in recursion and induction. In addition to theorem proving, I will also talk about how can you design syntax and notations to make your formalization more readable and maintainable.

Zoom link: https://nus-sg.zoom.us/j/84932999912?pwd=tSka7Th1z2McUW3zhjquuUQ7hcLfab.1
Zoom ID: 849 3299 9912
Pwd: 475364

Add to calendar :

Date/Time : 21 Feb 2025 11:00
Venue : S17 #04-04 (SR3)
Speaker : Wang Yutong, National University of Singapore

In the third lecture, we will learn how to construct new mathematics objects in Lean. Although Mathlib4 has provide numerous amount of objects and definitions, we always need to build our own infrastractures when formalizing a new aspect. In this course, we will use examples in undergraduate calculus and Gaokao to demonstrate how to properly design the infrastracture. Specifically, we will together explore the usage of class, structure, as well as their combination with definitions and theorems to compose a reasonable formalization project.

This mini-course will live stream. Here are the zoom ID and the link:
https://nus-sg.zoom.us/j/81322620719?pwd=Wg8FVTZbfX4QpZ7vbiYwaBN3n1MO7A.1

Meeting ID: 813 2262 0719
Passcode: 359631

Add to calendar :

Date/Time : 14 Feb 2025 11:00
Venue : S17 #04-04 (SR3)
Speaker : Wang Yutong, National University of Singapore

When formalizing problems in high-school and undergraduate level, we encounters different types of formulas and equalities from time to time, and one of the most critical steps is to simplify and solve them in efficient ways. This is also the step where most beginners feel tedious and challenging. In this course, we will dive into tactics like simp, linarith, norm_num, group, ring, etc to make the process easier. If time permitted, we will also briefly explain how you can design your own tactics to provide further simplifications. Various examples and practices will be given in this course.

This mini-course will live stream. Here are the zoom ID and the link:
https://nus-sg.zoom.us/j/81322620719?pwd=Wg8FVTZbfX4QpZ7vbiYwaBN3n1MO7A.1

Meeting ID: 813 2262 0719
Passcode: 359631

Add to calendar :

Date/Time : 07 Feb 2025 11:00
Venue : S17 #04-04 (SR3)
Speaker : Wang Yutong, National University of Singapore

In the first course, we will briefly introduce Lean 4 and verifiable mathematics, then go through together some general usages of LLM assistants to speed up mathematics research, including techniques like in-context-learning and function calling. Then we will use examples to demonstrate how these techniques, combined with expert knowledge and symbolic tools, can contribute to both formal and informal mathematics. Specifically, we will try together some recent tools in Lean 4, to effectively drive formal proof-writing in subsequent courses.
This mini-course is designed for general audiences without a background in LEAN.

This mini-course will live stream. Here are the zoom ID and the link:
https://nus-sg.zoom.us/j/81322620719?pwd=Wg8FVTZbfX4QpZ7vbiYwaBN3n1MO7A.1

Meeting ID: 813 2262 0719
Passcode: 359631

Add to calendar :

Date/Time : 23 Jan 2025 15:00
Venue : S17 #04-06 (SR1)
Speaker : Liu Beibei, Ohio State University

The critical exponent is an important numerical invariant of discrete isometry groups acting on symmetric spaces of non-compact type. In this talk, I will explain how the numerical invariant is closely related to geometry, dynamics, and representation of the group action in rank 1 symmetric spaces. On the higher rank side, I will focus on the comparison of critical exponent with other quantities such as Benoist limit cone and cubic differential under the deformation of surface group representations in the Lie group PSL(n, R).

Add to calendar :

Date/Time : 21 Jan 2025 15:00
Venue : S17 #04-06 (SR1)
Speaker : Yusuf Baris Kartal, University of Edinburgh

Morse theory provides a method for studying the topology of smooth manifolds through the critical points of a function and its gradient flow. In the 1980s, Andreas Floer applied ideas from Morse theory to the infinite dimensional setting, producing an invariant in symplectic topology that has since become a central tool in this field, and later understood to be closely related to enumerative geometry and mirror symmetry. Inspired by Floer’s insight, Cohen-Jones-Segal proposed a framework to obtain finer information from the data arising in Morse and Floer theory. However, this setup is not a priori compatible with the compact group actions, which limits their usefulness in the study of equivariant topology and geometry. In this talk, I will explain how, in joint work with Laurent Cote, we extend the setup and the construction of Cohen-Jones-Segal to study equivariant invariants. I will then discuss applications to topology and symplectic geometry, and explain how tools from homotopy theory can be used to relate symplectic invariants to the topology of the underlying manifold.

Add to calendar :

Date/Time : 20 Jan 2025 09:00
Venue : Zoom link TBA
Speaker : Yangyang Li, The University of Chicago

Minimal surfaces, which generalize geodesics to higher dimensions, naturally model various physical phenomena and are fundamental tools in geometric analysis. In this talk, I will survey recent advances on the existence, regularity, and Morse-theoretic study of minimal (hyper)surfaces. Highlights include our recent results on the enumeration of minimal surfaces, the generic regularity of minimal hypersurfaces, and their anisotropic counterparts. I will also discuss how these findings illuminate the interplay between the space of minimal hypersurfaces and the ambient Riemannian manifold.

Add to calendar :