BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Riccardo Brasca (Université Paris-Cité)
DTSTART:20221026T180000Z
DTEND:20221026T193000Z
DTSTAMP:20260412T170544Z
UID:ProofUSACH/1
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/ProofUSACH/1
 /">An introduction to formalized mathematics: why it is interesting?</a>\n
 by Riccardo Brasca (Université Paris-Cité) as part of An introduction to
  proof assistants: a mini course about mathematical formalization\n\nLectu
 re held in Auditorio Piso -1.\n\nAbstract\nFormalization is the process of
  <i>digitalizing</i> mathematical results\, teaching them to a computer. W
 e will explain how this process is done\, explaining the general philosoph
 y behind it\, and why it is interesting for people interested in ``standar
 d'' mathematics. Indeed\, formalization has several benefits\, the most ob
 vious being the verification of the correctness of theorems beyond a reaso
 nable doubt\, starting from the axioms. I will explain in detail what this
  means\, and also why I think there are others\, even more important\, adv
 antages of formalized mathematics. This is not a course in logic nor found
 ations of mathematics\, in particular no prior knowledge of these topics i
 s needed.\n
LOCATION:https://researchseminars.org/talk/ProofUSACH/1/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Riccardo Brasca (Université Paris-Cité)
DTSTART:20221027T180000Z
DTEND:20221027T193000Z
DTSTAMP:20260412T170544Z
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
BEGIN:VEVENT
SUMMARY:Riccardo Brasca (Université Paris-Cité)
DTSTART:20221102T143000Z
DTEND:20221102T160000Z
DTSTAMP:20260412T170544Z
UID:ProofUSACH/3
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/ProofUSACH/3
 /">Examples and exercises about formalization mathematics in Lean</a>\nby 
 Riccardo Brasca (Université Paris-Cité) as part of An introduction to pr
 oof assistants: a mini course about mathematical formalization\n\n\nAbstra
 ct\nI will give several examples of formalization of small results in Lean
 \, both starting from scratch and using Mathlib. The goal of this final da
 y is to let the audience ''play'' with Lean in practice\, proving real wor
 ld theorems.\n
LOCATION:https://researchseminars.org/talk/ProofUSACH/3/
END:VEVENT
END:VCALENDAR