6 MAR 2025
14:00 - 16:00

Mathematicians have used machines and datasets to aid their research for millennia. In our time, computational tools such as computer algebra systems, SAT/SMT solvers, Reinforcement Learning, and LLMs play an increasingly central role in mathematical discovery. Complementing these, formal verification and proof assistants ensure the correctness of mathematical arguments, providing mathematicians with instant and extremely high confidence in formalized results and enabling large-scale collaboration. This formal proof revolution is transforming how we produce, organize, and interact with mathematical knowledge.
In this talk, I will introduce Lean, a popular proof assistant based on dependent type theory. I will give an overview of Lean's community-based mathematical library Mathlib. I will survey the state of the art in using Lean in mathematical research. Finally, I will highlight Lean's powerful metaprogramming framework, and how we are employing it in a new collaborative project to bring Homotopy Type Theory (HoTT) and synthetic homotopical reasoning into Lean4.

Zoom room information:
https://us06web.zoom.us/j/81916335336?pwd=5zQT4lutMiBoY5Xp1pkFGtbqiaGozg.1
Meeting ID: 819 1633 5336
Passcode: 559618
Venue: Niavaran, Lecture Hall 1

5 MAR 2025
17:30 - 19:00

Seen through the lens of the Minimal Model Program, the classification of algebraic varieties can be summarised into two main steps: firstly, the algorithm of the MMP allows to decompose a variety with mild singularities, birationally, into a tower of fibrations whose general fibres have ample, anti-ample, or numerically trivial canonical divisor. In view of this decomposition, the natural second step to take is to study these 3 classes of algebraic varieties in detail, for example, studying their moduli theory and/or any other property that could shed light on ways to understand all possible elements that belong to such classes. It turns out a very important property to understand in this process is boundedness: a collection of varieties is bounded when the elements of the given collection can be parametrised using a finite type geometric space. The property of boundedness plays a crucial role in the construction of proper moduli spaces of finite type. Moreover, if a given collection of algebraic varieties is bounded (in char 0), then the topological types of their underlying analytic spaces belong to only finitely many homeomorphism classes: hence, all of their topological invariants come in just finitely many possible different versions. While over the past 15 years, several breakthroughs have completely settled the question of boundedness (and the subsequent construction of moduli spaces) in the case of log canonical models (varieties/pairs with ample canonical divisor) and Fano varieties (those with anti-ample canonical divisor), the situation is still quite unclear in the case of trivial numerical divisor. In this seminar, I will try to explain what is known, or not, and what those challenges are that make the situation quite more complicated than the other 2 cases. I will moreover explain how we can overcome most of the issues if we assume that a K-trivial variety is endowed with a fibration structure of relative dimenesion one. The seminar includes results from various works I developed over the past 10 years with G. Di Cerbo, C. Birkar, S. Filipazzi, and C. Hacon. Moreover, I will talk about current work in progress with P. Engel, S. Filipazzi, F. Greer, M. Mauri were we show various new boundedness results for K-trvial varieties fibered in K3 surfaces or abelian varieties.

https://zoom.us/join
Meeting ID: 9086116889
Passcode: 362880
Website: http://math.ipm.ac.ir/agnt/
Venue: , (Zoom Lecture)

5 MAR 2025
14:00 - 15:00

Locally recoverable codes (LRCs) play a vital role in distributed storage systems where the failure or unavailability of storage devices is a common occurrence. The purpose of LRCs is to facilitate the repair processes required to recover lost or damaged data in such systems. In this talk, we discuss new constructions of (r, δ)-LRCs. Initially, we provide generator matrices for (r, 2)-LRCs, which is Singleton-Type Bound (STB)-optimal. Also, we present a method for recovering an erased symbol in a codeword of our (r, 2)-LRC. We argue an example illustrating that the Gray image of particular Z_{p^{s+1 }} -LRCs of length n results in LRCs of length np^s over F_p, which may not necessarily be linear. This introduces a novel class of LRCs, prompting further exploration of the connections between existing nonlinear LRCs in finite fields and linear ring-based LRCs. Next, we present the parity-check matrices for another family of (r, δ)-LRCs over Z_{p^s} and construct two instances of STB-optimal (r, δ)-LRCs.

Zoom room information:
https://us06web.zoom.us/j/84906984159?pwd=BCWaIbXBuku3A5I84zNg9mHFxVZjXD.1
Meeting ID: 849 0698 4159
Passcode: 362880
Venue: Niavaran, Lecture Hall 1

26 FEB 2025
16:00 - 17:00

The concept of hypergeometric functions was coined by John Wallis in the middle of 17th century as a generalization of many elementary functions. Since then, these functions have played a key role in various branches of mathematics. Great mathematicians such as Euler, Gauss, Riemann and Klein have investigated the theory of hypergeometric functions from various aspects and have shown the role of these functions in the connection of differential equations, geometry and number theory. In the 20th century, with the generalizations of these functions, unexpected applications of them in theoretical physics (string theory) were found, which led to the solution of conjectures in enumerative geometry. In this lecture, we will have a general overview of these efforts.

Subscribing the Mathematics Colloquium mailing list:
https://groups.google.com/g/ipm-math-colloquium
Venue: Niavaran, Lecture Hall 1

26 FEB 2025
14:00 - 15:00

A connected graph, on four or more vertices, is matching covered if every edge is present in some perfect matching. An ear decomposition theorem (similar to the one for 2-connected graphs) exists for bipartite matching covered graphs due to Hetyei (1964). From the results and proofs of Lovasz and Plummer, that rely on Hetyei's theorem, one may deduce that any minimal bipartite matching covered graph has at least 2(m − n + 2) vertices of degree two (where minimal means that deleting any edge results in a graph that is not matching covered); such a graph is said to be extremal if it attains the stated lower bound.
We provide a complete characterization of the class of extremal minimal bipartite matching covered graphs. In particular, we prove that every such graph G is obtained from two copies of a tree devoid of degree two vertices, say T and T ′ , by adding edges - each of which joins a leaf of T with the corresponding leaf of T ′ . Apart from the aforementioned bound, there are four other bounds that appear in, or may be deduced from, the work of Lovasz and Plummer. Each of these bounds leads to a notion of extremality. We obtain a complete characterization of all of these extremal classes and also establish relationships between them. Two of our characterizations are in the same spirit as the one stated above. For the remaining two extremal classes, we reduce each of them to one of the already characterized extremal classes using standard matching theoretic operations.
This is joint work with Amit Kumar Mallik (who was a student at IIT-B at the time) and the late Ajit A. Diwan (IIT-B). Our manuscript is available here: https://arxiv.org/ abs/2404.06445. I will present the necessary background, and describe and prove (some of) our aforementioned results. The talk will be self-contained.

Zoom room information:
https://us06web.zoom.us/j/84906984159?pwd=BCWaIbXBuku3A5I84zNg9mHFxVZjXD.1
Meeting ID: 849 0698 4159
Passcode: 362880
Venue: Niavaran, Lecture Hall 1

20 FEB 2025
14:00 - 16:00

We will introduce a class of models of Axiom of Determinacy that we call Nairian Models and will explain their role in set theory.

Zoom room information:
https://us06web.zoom.us/j/81916335336?pwd=5zQT4lutMiBoY5Xp1pkFGtbqiaGozg.1
Meeting ID: 819 1633 5336
Passcode: 559618
Venue: Niavaran, Lecture Hall 1

19 FEB 2025
17:30 - 19:00

We discuss construction of a derived Lagrangian intersection theory of moduli spaces of perfect complexes, with support on divisors on compact Calabi Yau threefolds. Our goal is to compute deformation invariants associated to a fixed linear system of divisors in CY3. We apply a Tyurin degeneration of the CY3 into a normal-crossing singular variety composed of Fano threefolds meeting along their anti-canonical divisor. We show that the moduli space over the Fano 4 fold given by total space of degeneration family satisfies a relative Lagrangian foliation structure which leads to realizing the moduli space as derived critical locus of a global (-1)-shifted potential function. We construct a flat Gauss-Manin connection to relate the periodic cyclic homology induced by matrix factorization category of such function to the derived Lagrangian intersection of the corresponding ?Fano moduli spaces?. The later provides one with categorification of DT invariants over the special fiber (of degenerating family). The alternating sum of dimensions of the categorical DT invariants of the special fiber induces numerical DT invariants. If there is time, we show how in terms of ?non-derived? virtual intersection theory, these numerical DT invariants relate to counts of D4-D2-D0 branes which are expected to have modularity property by the S-duality conjecture. This talk is based on joint work with Ludmil Katzarkov and Maxim Kontsevich, recent work with Jacob Krykzca, and former work with Vladimir Baranovsky.

https://zoom.us/join
Meeting ID: 9086116889
Passcode: 362880
Website: http://math.ipm.ac.ir/agnt/
Venue: Niavaran, Lecture Hall 1

19 FEB 2025
15:30 - 17:00

The pants graph of a compact orientable surface S, introduced by Hatcher and Thurston, is a simplicial graph whose vertices are maximal essential multicurves on S and whose edges correspond to certain local moves on multicurves. The importance of the pants graph comes from a theorem of Brock showing that the pants graph is a good combinatorial model for the Teichmuller space with the Wiel-Petersson metric, which is the space of hyperbolic metrics on S up to isotopy. In joint work with Marc Lackenby, we give upper bounds for distance in the pants graph and derive applications for distance in the Teichmuller space and also for volumes of hyperbolic 3-manifolds. I will give an overview of these results, no prior familiarity with the Teichmuller is needed for the talk.

Online via Zoom:
Meeting ID: 908 611 6889
Passcode: 362880
Venue: Niavaran, Lecture Hall 1

19 FEB 2025
14:00 - 15:00

Many combinatorial optimization problems have been studied in the prize collecting setting, where the coverage requirement for an entity can be relaxed by paying a predefined penalty. This resembles the classical Lagrangian relaxation, and is natural in many practical applications. In this talk we discuss approximation algorithms for the prize-collecting version of the Traveling Salesman Problem (TSP) and some of its generalizations.

Zoom room information:
https://us06web.zoom.us/j/84906984159?pwd=BCWaIbXBuku3A5I84zNg9mHFxVZjXD.1
Meeting ID: 849 0698 4159
Passcode: 362880
Venue: Niavaran, Lecture Hall 1