Fall 2024 (Current Semester)

The colloquium meets on Tuesdays at 2:40pm, unless otherwise stated.

• September 24th

  Julia Kameryn Williams (Bard College at Simon’s Rock)

  Infinity, the axiom of choice, and mediacy

  What does it mean to be finite? To be infinite? Why does the axiom of choice come into the picture? What even is the axiom of choice? What weird and exciting things happen when we try to generalize the ideas which answer these questions? We will discuss these questions and more. [flyer] [slides here]

• October 8th

  Alex Van Abel (Wesleyan University)

  Pseudofinite Model Theory

  In model theory, we study mathematical structures and the things we can say about them – classically, in first-order logic. Pseudofinite structures are infinite mathematical structures that “behave like” finite structures. In this talk, I will outline the basics of model theory and first-order logic, and clarify what I mean by “behave like” in the previous sentence. I will illustrate pseudofiniteness with some examples and non-examples, and share some instances of how pseudofinite model theory has been used to answer concrete questions in combinatorics. [flyer]

• December 3rd

  Astra Kolomatskaia (Wesleyan University)

  Talk 1: What is type theory? (1:30pm)

  This talk is an introduction to formal logic and type theory. We begin by considering minimal logic, a logical system in which the only compound propositions are of the form $T \rightarrow W$ [$T$ implies $W$]. We discuss the notions of truth and proof, and, thinking about an efficient way to express proof, reformulate the system into the form of a type theory. We then interpret terms of the type theory as programs in a programming language, and discuss one algorithm for “running” these programs that is based on the semantic/categorical properties of our language. [talk 1 slides]

  Talk 2: What is a triangle? (3:30pm)

  If you imagine some abstract space, then you can imagine marking off points in this space, drawing lines [i.e. any squiggly path] connecting two points, and shading in triangular surfaces bounding three lines. This data forms an example of a semi-simplicial type, which, intuitively, is an abstract specification of what the words “point, line, triangle, etc.” mean. If the collections of points, lines, triangles, etc. are all “sets”, then the object that they define is an example of a semi-simplicial set, and this notion is central to geometry and topology. However, if we more generally consider the collections of points, lines, triangles, etc. to be something like “spaces”, then there arises a very subtle problem of coherently assembling an infinitely hierarchical structure from the data of n-simplicies at each level. This problem exists purely from the perspective of homotopy theory, but is most evident from the perspective of type theory – here, the challenge can be made very concrete: to write a definition of semi-simplicial types as code in a proof assistant.

  The problem of defining semi-simplicial types was one of the most important open problems in homotopy type theory. It was identified at the emergence of the field by Vladimir Voevodsky, and remained open for the next twelve years. In this talk, we present a solution to this problem in the form of Displayed Type Theory [dTT]. dTT is a new multi-modal homotopy type theory that enables the construction of semi-simplicial types in full semantic generality. It answers the question “What is a triangle?” by asking “What is mathematics?”, taking that answer, and building a new universe for mathematics in which “everything is a triangle” [i.e. a diagram model on the augmented semi-simplex category]. Then, using language specific to this new mathematical universe, we are able to state a novel coinductive universal property for semi-simplicial types which is “finitary/uniform”. Taking the discrete part of this diagram yields semi-simplicial types in the starting model, and the universal property furnishes this object with computational meaning in a way that enables working with semi-simplicial types on a computer.

  This talk is joint work with Mike Shulman. [flyer] [talk 2 slides]

Spring 2024

The colloquium meets on Thursdays at 2:40pm, unless otherwise stated.

• February 29th

  Jack Burkart (Bard College at Simon’s Rock)

  The Carpenter’s Rule Problem

  Is it possible to take any given polygon and move it through space to a convex polygon, while never having the polygon intersect itself? If you drop a necklace on a flat table and attempt to do this yourself, you’ll probably be able to successfully do this. This is far from a mathematical proof, however, and this problem, known as the Carpenter’s Rule Problem, remained open for decades until it was solved in the early 90s. In this talk, I’ll introduce the Carpenter’s rule problem and explain a surprising approach for how to solve it that involves an important technique in optimization known as linear programming. Most of this talk should be approachable for anyone who enjoys looking at pictures and has taken a calculus course. [flyer]

• March Canceled

  Lauren Rose (Bard College)

  Canceled

• April 25th

  Matt Ollis (Emerson College)

  Uniquely Completable Partial Latin Squares

  A latin square of order $n$ is an $n \times n$ array in which each symbol from a set of order $n$ appears exactly once in each row and exactly once in each column. If we loosen the definition so that each symbol appears at most once in each row and at most once in each column (and so there may be empty cells) then we have a partial latin square. A partial latin square is uniquely completable if there is exactly one way to fill in the empty cells to obtain a latin square.

  We look at some historical and recent work related to uniquely completable partial squares. Motivating questions include: how few entries can a uniquely completable partial latin square have? How many can one have, if it is minimal in the sense that removing any entry allows multiple completions? What if we add extra conditions (like a sudoku puzzle does)? Does it make sense to ask about infinite latin squares? There are many accessible open problems.

  Includes joint work with Aurora Callahan, Emma Hasson, Kaethe Minden and Yolanda Zhu. [flyer] [slides]