Seminar

A formalization of forcing and the consistency of the failure of the continuum hypothesis

Abstract:

Forcing is a technique for constructing new models of set theory where certain statements are "forced" to be true or false, e.g. the axiom of choice, or the continuum hypothesis. We describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover. As an application of our framework, we specialize our construction to a Boolean completion of the Cohen poset and formally verify in the resulting model the failure of the continuum hypothesis. This is joint work with Floris van Doorn.

Seminar/Colloquia Event Item 3435

I will review the endeavors of many great mathematicians of the late 19th century and beginning of the 20th century, and their motivating philosophies in pursuing a consistent and complete axiomatic system for mathematics. On the way, they encountered many paradoxes, such as Russell's, with important implications for our mathematical understanding.  

Large Deviations Principle for Stochastic Partial Differential Equations in Fluid Dynamics

Abstract:

Large (and moderate) deviations principle identifies the exponential rate of decay of probabilities for rare events in the context of small noise asymptotics. For a class of nonlinear stochastic partial differential equations that arise in fluid dynamics, I will present weak convergence approach to identify the exponential rate.