Introduction to Lean theorem prover
SUURI-COOL (Kyushu) セミナー
開催期間
2025.10.31(金)
14:00 ~ 17:00
14:00 ~ 17:00
場所
Online via Zoom / 理化学研究所
講演者
水野 勇磨 (Postdoctoral Researcher, University College Cork, Ireland)
概要
https://ithems.riken.jp/ja/events/introduction-to-lean-theorem-prover
A theorem prover is a tool for the formalization of mathematics, that is, for rigorously expressing and verifying theorems and proofs on a computer. In recent years, the Lean theorem prover has seen progress in the formalization of a wide range of areas of mathematics. In this talk, I will explain formalization of mathematics in Lean from the basics and survey the formalized results achieved to date.