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. 

Abstract: