Seminar

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.

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.  

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. 

notice the special date. March 19th, 9-10am. Room Thackeray 427

Abstract:

The Navier-Stokes equations (NSE) model the motion of incompressible viscous fluids and are widely used in engineering and physics, etc. In many applications, the time-averaged information is very often the quantity of interest, so this talk focuses on finding the numerical solutions  of the steady Navier-Stokes equations (SNSE). We introduce a few improvements to the commonly used Picard iteration for solving the SNSE  from different aspects, like shortening the required number of iterations and reducing the computational cost for each iteration.