Introduction to Lean theorem prover
- 日時
- 2025年10月31日(金)14:00 - 17:00 (JST)
- 講演者
-
- 水野 勇磨 (Postdoctoral Researcher, University College Cork, Ireland)
- 会場
- via Zoom
- セミナー室 (359号室) 3階 359号室
- 言語
- 英語
- ホスト
- Taketo Sano
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.
このイベントは研究者向けのクローズドイベントです。一般の方はご参加頂けません。メンバーや関係者以外の方で参加ご希望の方は、フォームよりお問い合わせ下さい。講演者やホストの意向により、ご参加頂けない場合もありますので、ご了承下さい。