Monday, December 3rd; 5:15pm

Presented by Daoji Huang.

A formal proof is a proof in which every logical inference has been checked all the way back to the fundamental axioms of mathematics. Although there is a long way to go for formalization to be practical for working mathematicians, existing theories and technologies of formal verification are already capable of formalizing a large body of modern mathematics. In this talk, I will introduce the building blocks of formal verification, including logical foundations, proof assistants, and expressing mathematics formally in such systems. In particular, I will illustrate the relevant concepts by giving a brief overview of type theories, the Coq proof assistant, and the Flyspeck project that formally verified the 400 years old Kepler’s Conjecture on sphere packing. Furthermore, I will discuss common challenges in formalization endeavors.

Monday, November 26th; 5:15pm

Presented by Professor Bob Connelly.

Put a bunch of circular disks in a container and squeeze the container until they jam. What does the packing look like? What can you say about the density of the packing? When the disks are the same size and the container is a flat torus, the answer is known. If the Radii in ratio 1:2:3, density = 7π/24=0.92015.. sizes are random as with granular materials, for existence, there will be a minimum number of contacts. If the graph of contacts is a triangulation, often the density of the packing is quite large. Evan Solomonides and Maria Yampolskaya will demonstrate a simulation of packings as the container contracts until they jam.

Monday, November 19th; 5:15pm

Presented by Jack Cook.

Using the tools of smooth manifold theory, we propose a generalized framework for olfactory reception, learning, and processing. Inspection of the tangent bundle to a manifold yields vector fields which allow for quantification of changes. We utilize group actions to discover fibre bundles over the manifold and discover various properties related to learning. Under this paradigm, we develop a method for categorization as well as analytical tools to model changes in the category. We end with a quick discussion of searching for data on the manifold in a way that beats ``nearest neighbour.''

Monday, November 12th; 5:15pm

Presented by Jessie Tan.

The Weil Conjectures are four statements about an analogue of the Zeta function over finite fields. I’m going to talk about the roots of polynomial equations in a “mod p” setting, define the zeta function for a projective variety, and with the new vocabulary I’ll state the Weil Conjectures at the end. Familiarity of finite fields and projective geometry is useful but not required.

Monday, November 5th; 5:15pm

Presented by Seraphina Lee.

Elliptic curves are a special kind of curve that can be given as solutions to equations of the form y^2+a_1xy+a_3y=x^3+a_2x^2+a_4x+a_6, with an added point at infinity. I will begin with an introduction to basic definitions, followed by a discussion of their significance, plus what we know (and don't know) about the group structure on their Q- and F_p-points.

Undergraduate Math Reception

Monday, October 22nd; 4pm

Come talk to professors, figure out what classes to take, and hear about study abroad programs for math, the Putnam and Math Modeling Competitions, and other fun math things!