Date/Time : 17 Oct 2024 16:00
Venue : S17 #05-12 (SR4)
Speaker : Wang Yutong, National University of Singapore

The growing of verifiable formal languages, particularly interactive proof assistants like Lean 4, is shaping the future of mathematics and transforming how large language models (LLMs) can assist in automated reasoning. However, navigating the vast and complex Mathlib and composing reliable formal statements remains a challenge, with arcane syntax and scattered lemmas.

In this talk, I will present our recent developments: the LeanSearch platform V2 and the Herald translator, which features Lean-aware LLMs to streamline proof writing and auto-formalization of statements. We will explore specialized model training and data augmentation techniques that enhance LLM-accelerated formalization. I will demonstrate how these tools can assist both mathematicians and Lean developers.

Add to calendar :

Date/Time : 14 Aug 2024 16:00
Venue : S17 #06-11 (SR6)
Speaker : Felix Schremmer, The University of Hong Kong

This talk presents a novel, interdisciplinary study that leverages a Machine Learning (ML) assisted framework to explore the geometry of affine Deligne-Lusztig varieties (ADLV). The primary objective is to investigate the nonemptiness pattern, dimension and enumeration of irreducible components of ADLV. Our proposed framework demonstrates a recursive pipeline of data generation, model training, pattern analysis, and human examination, presenting an intricate interplay between ML and pure mathematical research. Notably, our data-generation process is nuanced, emphasizing the selection of meaningful subsets and appropriate feature sets. We demonstrate that this framework has a potential to accelerate pure mathematical research, leading to the discovery of new conjectures and promising research directions that could otherwise take significant time to uncover. We rediscover the virtual dimension formula and provide a mathematical proof of a newly identified problem concerning a certain lower bound of dimension. This is joint work with Bin Dong, Xuhua He, Pengfei Jin and Qingchao Yu, and the corresponding paper can be found on arXiv and the Peking Mathematical Journal.

Add to calendar :

Date/Time : 12 Aug 2024 15:00
Venue : S17 #04-06 (SR1)
Speaker : Daniel Bartl, University of Vienna

A major challenge in modern optimization problems is their instability, where small data perturbations can have disproportionately significant effects. We address this challenge in two settings. First, we focus on a distributionally robust approach, a popular method to counteract instability generically using optimal transport. Specifically, we demonstrate how this approach can systematically quantify the (in-)stability of a given optimization problem. In the second part, we focus on statistical robustness, dealing with data subject to outliers, such as those caused by adversarial corruption. We design robust estimators for optimization problems and risk measures.

Add to calendar :

Date/Time : 08 Jul 2024 16:00
Venue : S17 #04-06 (SR1)
Speaker : Panel Discussion: Various speakers,

The leap from higher education to industry is a pivotal stage for many graduate students. Emphasising the necessity of an interdisciplinary approach and the application of the robust analytical skills honed during graduate studies, this panel discussion offers a comprehensive exploration of the journey that awaits MSc and PhD graduates who are looking to bridge the gap between academic accomplishment and professional fulfilment in the industry. Panellists will provide candid reflections on their personal pathways, highlighting the obstacles they encountered and the successes they achieved within various industrial domains. Attendees of the session will be encouraged to engage with live inquiries and raise pertinent topics for discussion. Discussions will revolve around the symbiotic relationship between advanced academic preparation and industry expectations, strategic planning for entering the corporate sector, the diverse opportunities ranging from employment in small to large-scale organisations to the launch of deep tech ventures, as well as the innovative trends and fruitful careers found in today’s industrial research and development.

Add to calendar :

Date/Time : 19 Apr 2024 10:00
Venue : S17 #04-06 (SR1)
Speaker : Riccardo Brasca, Université Paris Cité

Workshop on Formal Proofs and Lean

Add to calendar :

Date/Time : 17 Apr 2024 10:00
Venue : S17 #04-06 (SR1)
Speaker : Riccardo Brasca, Université Paris Cité

Workshop on Formal Proofs and Lean

Add to calendar :

Date/Time : 15 Apr 2024 10:00
Venue : S17 #04-06 (SR1)
Speaker : Riccardo Brasca, Université Paris Cité

Workshop on Formal Proofs and Lean

Add to calendar :

Date/Time : 06 Feb 2024 10:00
Venue : S17 #04-06 (SR1)
Speaker : Ian Gleason, Universitat Bonn

The local Langlands correspondence, proposed by Langlands as the non-abelian analogue of local class field theory for non-Archimedean local fields, has been established for various reductive groups over the years. However, a construction in full generality was lacking until the recent proposal by Fargues and Scholze, who introduced semi-simplified Langlands parameters for every reductive group. Their construction employs Scholze’s theory of diamonds, a modern approach to p-adic analytic geometry. This talk begins by revisiting historical developments in number theory that led to the formulation of the local Langlands correspondence. Subsequently, we explore the relevance of p-adic analytic geometry to the study of the local Langlands program and the impact these innovative methods have on our comprehension of the local Langlands correspondence.

Add to calendar :

Date/Time : 01 Feb 2024 15:00
Venue : S17 #04-06 (SR1)
Speaker : Zhang Jiacheng, University of California, Berkeley

In this talk, we are going to talk about recent development on Stackelberg equilibrium and Mean Field Game. Stackelberg game has attracted recent interest modeling an asymmetric, general sum game between leaders and followers.

Firstly, we consider a discrete-time Stackelberg mean field game (SMFG) with one leader and an infinite number of homogeneous followers via optimization lense.We focus on a robust setting where the followers have bounded rationality and only aim at achieving some ε-Nash equilibrium (NE) while the leader wants to maximize her objective in the worst case scenario among all ε-NEs. We study the sensitivity analysis when the leader only has access to some perturbed model. We show that the value function is unstable with respect to the perturbation of the model and the leader needs to be more pessimistic and solve a relaxed problem to obtain a near optimal solution. The analysis is done by formulating this SMFG problem into an explicit minimax optimization problem and studying the sensitivity property using the optimization framework.

Second, we investigate the existence of an optimal policy to monitor a mean field system of agents managing a risky project under moral hazard with accidents modeled by L ́evy processes magnified by the law of the project. We provide a general method to find both a mean field equilibrium for the agents and the optimal compensation policy under general, sufficient and necessary assumptions on all the parameters. We formalize the problem as a bilevel optimization with the probabilistic version of a mean field game which can be reduced to a controlled McKean-Vlasov SDE with jumps. We apply our results to an optimal energy demand-response problem with a crowd of consumers subjected to power cut/shortage when the variability of the energy consumption is too high under endogenous or exogenous strains. In this example, we get an explicit solution to the mean field game and to the McKean-Vlasov equation with jumps.

Add to calendar :