Seminar
Spectral Methods of Graphs for Data Sets of Mixed Dimensions
On the Upper Bound of the Cardinality of Topological Spaces
Davide Giovagnoli - Free boundary regularity for the inhomogeneous Stefan Problem
Spread Statistics as a Function of Small Cycles
Numerical Analysis of a Corrected Smagorinsky Model
For more information, please visit the Pitt AWM webpage.
A Multiscale Mixed Modeling Framework of Parasitoid Wasp and Host Dispersal
For more information, please visit the Pitt AWM Chapter webpage.
Intro to Proof Assistants, Examples with Lean
In this talk, we will explore the practical uses of a proof assistant for mathematicians. In particular, we will learn how to formalize a variety of propositions in the proof assistant Lean 4. Through these examples, we will learn how to convert our familiar strategies into the different proof tactics which have been implemented in Lean. Additionally, we will discuss why they are called proof assistants and the different ways that they make proving things easier. Finally, we’ll touch on some theory behind proof assistants and their role in modern mathematics.