A formalization of mathematical analysis in Rocq prover (Delivered in English)
- LecturerDr. Takafumi Saikawa (Nagoya University, Japan)
Host: Shin-Cheng Mu - Time2025-03-24 (Mon.) 14:00 ~ 16:00
- LocationAuditorium101 at IIS new Building
Abstract
I will present Mathcomp-Analysis, a formalization of mathematical analysis in Rocq prover (formerly known as Coq proof assistant).
The talk will cover basic definitions such as topological spaces and real numbers, and recent developments on the measure-theoretic probability theory.
The talk will cover basic definitions such as topological spaces and real numbers, and recent developments on the measure-theoretic probability theory.