Date/Time : 17 Sep 2025 16:00
Venue : S17 #04-04 (Seminar Room 3)
Speaker : Luo Tao, Shanghai Jiao Tong University

Artificial Intelligence for Mathematics (AI4Math) is a rapidly advancing field with significant implications for both academic research and industrial applications. In this talk, we will review the evolution of AI-driven mathematical reasoning, tracing the transition from intuitive, natural language-based approaches to the rigorous, verifiable proofs enabled by formal languages. After providing a foundational overview, we conduct a technical survey of three key research frontiers within the formal systems: Automated Theorem Proving, Autoformalization, and Automated Semantic Evaluation. The primary focus is placed on our contributions to the latter two areas, which are crucial for bridging the gap between human mathematical knowledge and machine-verifiable logic.

Add to calendar :

Date/Time : 25 Jun 2025 10:00
Venue : IMS Executive Seminar Room (S17 Level 3)
Speaker : François Loeser, Sorbonne University

We will provide a general overview of our work with E. Hrushovski on tame geometry over valued fields, using the stable completion of algebraic varieties over valued fields. A key result is the existence of retractions to piecewise-linear objects called skeleta, which are definably isomorphic to definable subsets of the value group. We will conclude by presenting a recent finiteness result obtained with A. Ducros, E. Hrushovski and J. Ye for tropical functions on such skeleta.

Add to calendar :

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 :