Ponente: Johannes Hölzl (Vrije Universiteit Amsterdam)
Lugar: Seminario Mirian Andrés (Edificio CCT)
Hora: jueves 16 de noviembre, 09:00
Resumen: I will present the current state of analysis in Lean 3. The formalization of the reals is based on the completion of uniform spaces, requiring a more extensive filter library. While the analysis in Lean is developed up to the Lebesgue measure, I mostly want to focus on topological spaces and measurable spaces, and compare their formalization with the one in Isabelle.
The slides of the talk are available from the following link.