Past Events

HyperTree Proof Search (HTPS) is the current state-of-the-art algorithm for automated theorem proving in Lean. I will go over Monte Carlo Tree Search and AlphaGo, and show how HTPS applies

A graph G is said to satisfy the Vizing bound if χ(G)≤ω(G)+1, where χ(G) and ω(G) denote the chromatic number and clique number of G, respectively. It was conjectured by

Erdős-Kleitman-Rothschild proved that the number of triangle-free graphs on n vertices is asymptotic to the number of bipartite graphs; or in other words, a typical triangle-free graph is a random

Explaining why the simplex method is fast in practice, despite it taking exponential time in the theoretical worst case, continues to be a challenge. Smoothed analysis is a paradigm for

We will discuss progress on formalizing the dependencies of one proof of the Pythagorean Theorem from Euclid's elements. The focus of the seminar will be putting these statements together, each

Social Choice Theory is a very broad topic, but I will outline some key definitions and results, including the infamous impossibility theorems for multicandidate voting. I'll also discuss some real-world

Each vertex of an arbitrary simple graph on n vertices chooses k random incident edges. What is the expected number of edges in the original graph that connect different connected

Computers are now very good at evaluating finite sums in closed form. They can do them almost instantly and can often prove that a sum cannot be evaluated in closed

In this talk, I will present a few results on a number of graph exploration problems in the following natural scenario: an algorithm starts exploring an undirected graph from some

When a finite statement in discrete maths is being extended to its infinite analogue, a useful method for brushing details under the rug is to say that we "use a

The many types in Lean are all defined inductively from a few type-forming rules (e.g. dependent products, lambda terms, and universes). I will go over what these rules are, how

Erdős' unit distance problem and Erdős' distinct distances problem are among the most classical and well-known open problems in all of discrete mathematics. They ask for the maximum number of

We give an introduction to recent advances in automating mathematics through automated formalization ("autoformalization") and proof-search using deep learning, specifically transformer-based large language models. Autoformalization is the process of automatically

Oblivious routing has a long history in both the theory and practice of networking. In this talk I will initialize the formal study of oblivious routing in the context of

As I'm sure you've all worked out by now, I really like making dumb jokes. Unfortunately, I can end up spending so much time on jokes that I don't end

This will be a workshop-style seminar. We will discuss choices relevant to formalizing proofs of the Pythagorean theorem, such as what extent to use synthetic geometry. We will also discuss

For a positive integer t, let F_t denote the graph of the t by t grid. Motivated by a 50-year-old conjecture of ErdÅ‘s about Turán numbers of r-degenerate graphs, we

For a finite set X, a family F of subsets of X is said to be increasing if any set A that contains B in F is also in F.

We study the basic statistical problem of testing whether normally distributed n-dimensional data has been truncated, i.e. altered by only retaining points that lie in some unknown truncation set S

This week, Professor Ian Jauslin will briefly discuss olean files. Then Professor Alex Kontorovich will continue the discussion from last week about Euclid's fifth book. In particular, we will discuss