Speaker: Arnav Kumar
Title: Dimension of posets and random graph orders
Abstract: A poset P = (X,P) is a set X equipped with a partial order P. The dimension of P is the minimum number of linear orderings on X required so that their intersection is P. We investigate two problems regarding the dimension of posets. The first problem is a conjecture by Bollobás and Brightwell from 1997 that the poset with a unicyclic cover graph has dimension at most 3. The second problem was proposed by Erdös in 1991 about the dimension of the random partial order obtained by taking the transitive closure of the random graph G(n,p), and the random bipartite graph B(n,n,p). The random graph order is a type of classical sequential growth model that physicists use to model relations of spacetime events in the Minkowski space, and thus finds its applications in the causal set approach to quantum physics.
Speaker: Elan Li
Title: Formalizing matroids induced from a matroid by a bipartite graph
Abstract: A result from Perfect in 1969 showed that given a finite matroid M and a bipartite graph where the ground set of this matroid is one of the partitions, one has that the other partition is also a matroid, with independent sets given by the graph and M. This construction can be used to show facts about matroid unions and matroid partitioning. We give a brief overview of the proof for this construction, and also how it is formalized in the Lean proof assistant.
Speaker: Max Jiang
Title: Formalizing a generalized Hall's marriage theorem
Abstract: Hall's marriage theorem is a well known result that characterizes exactly when a bipartite graph has a perfect matching. In 1971, Welsh showed a more general version of Hall's marriage by considering certain submodular functions over one side of the graph. Using this more general theorem, one can easily obtain the original Hall's marriage theorem, Hall's marriage with deficiencies, as well as Rado's theorem for matroids. We give an overview of these theorems, as well as present our work in formalizing these results in the Lean proof assistant.
Speaker: Kai Choi
Title: Index calculus over elliptic curves
Abstract: Index calculus is a family of randomized algorithms that solve the discrete logarithm problem, which is central in public-key cryptography. Efficient index calculus algorithms are known for some but not all groups. I will first discuss index calculus over the integers mod p (its classical setting) before discussing efforts made to adapt the algorithm to elliptic curves. Then, I will discuss work that I have done this term to implement, optimize, and measure the performance of different variants of the algorithm.