BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//IMPAN//Mathematics and AI//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Mathematics and AI
X-WR-TIMEZONE:Europe/Warsaw
BEGIN:VEVENT
UID:2026-11-05@mathandai.impan.pl
DTSTAMP:20261109T124644Z
DTSTART:20261105T131500Z
DTEND:20261105T141500Z
SUMMARY:Mathematics and AI: Marcin Pilipczuk – A gentle introduction to L
 ean 4 for mathematicians
LOCATION:IMPAN\, ul. Śniadeckich 8\, Warsaw\, room 321
DESCRIPTION:Marcin Pilipczuk (Faculty of Mathematics\, Informatics and Mech
 anics\, University of Warsaw)\nI will give a one-hour introduction to the 
 Lean 4 proof assistant\, aimed at mathematicians. We will cover:\n1) the 
 main theoretic concepts of Dependent Type Theory and the Curry–Howard eq
 uivalence\;\n2) how it is realized in Lean 4 and what the main design cho
 ices are\;\n3) a number of small examples of "human-made" formalizations i
 n Lean 4\;\n4) an overview of current capabilities of large reasoning mod
 els in writing Lean code\;\n5) a short discussion on the level of trust we
  can have towards Lean 4 proofs.\nhttps://mathandai.impan.pl/#2026-11-05
URL:https://mathandai.impan.pl/#2026-11-05
END:VEVENT
END:VCALENDAR