<!DOCTYPE html>
<html>
<head>
<title>Set Theory and Analysis</title>
</head>
<body>
<p>
Tuesday, 26 March 2024 - 10:00 to 11:30 <br />
Place: IM, konÃrna
</p>
<p>
Speaker: Igor Khavkine, IM CAS<br />
Title: Introduction to using the Lean proof assistant
</p>
<p class="ql-ed">
Abstract <br />
<p>In this informal lecture, I will give a quick practical introduction to using the Lean proof assistant. First, I will try to briefly explain the formal language that Lean uses (dependent type theory) and how it can encode both mathematical objects and logical statements/proofs. Second, I will go through the minimum practical steps you need set up Lean and start proving basic theorems. I will also try to touch on what formalized proofs can and can't do today for individual researchers.</p>
</p>
<p>
For more information see the seminar web page at <br />
https://www.math.cas.cz/index.php/events/seminar/6
</p>
<p>
Set Theory and Analysis mailing list <br />
settfa@math.cas.cz <br />
https://list.math.cas.cz/listinfo/settfa@math.cas.cz
</p>
</body>
</html>