A formalization of mathematical analysis in Rocq prover (以英文演講)
- 講者才川隆文 博士 (日本名古屋大學)
邀請人：穆信成 - 時間2025-03-24 (Mon.) 14:00 ~ 16:00
- 地點資訊所新館101演講廳
摘要
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.