BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Riccardo Brasca (Université Paris-Cité)
DTSTART:20221027T180000Z
DTEND:20221027T193000Z
DTSTAMP:20260412T203653Z
UID:ProofUSACH/2
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/ProofUSACH/2
 /">The Lean proof assistant</a>\nby Riccardo Brasca (Université Paris-Cit
 é) as part of An introduction to proof assistants: a mini course about ma
 thematical formalization\n\n\nAbstract\nThere are several software that ca
 n be used to formalize mathematics\, called <i>proof assistants</i>. One o
 f the most used today by mathematician is <i>Lean</i>: it has a huge libra
 ry of already formalized mathematics\, <i>Mathlib</i>\, that allows to tre
 at serious mathematics almost as we do ``on the blackboard''. I will expla
 in the basics of Lean and mathlib\, showing their how far we can go using 
 them. If time permits\, I will briefly mention some limitations and how th
 ey will be solved in the (hopefully near) future.\n
LOCATION:https://researchseminars.org/talk/ProofUSACH/2/
END:VEVENT
END:VCALENDAR