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:20260404T094503Z
UID:ProofUSACH/1
DESCRIPTION:Title: <a href="https://stable.researchseminars.org/talk/Proof
 USACH/1/">An introduction to formalized mathematics: why it is interesting
 ?</a>\nby Riccardo Brasca (Université Paris-Cité) as part of An introduc
 tion to proof assistants: a mini course about mathematical formalization\n
 \nLecture held in Auditorio Piso -1.\n\nAbstract\nFormalization is the pro
 cess of <i>digitalizing</i> mathematical results\, teaching them to a comp
 uter. We will explain how this process is done\, explaining the general ph
 ilosophy behind it\, and why it is interesting for people interested in ``
 standard'' mathematics. Indeed\, formalization has several benefits\, the 
 most obvious being the verification of the correctness of theorems beyond 
 a reasonable doubt\, starting from the axioms. I will explain in detail wh
 at this means\, and also why I think there are others\, even more importan
 t\, advantages of formalized mathematics. This is not a course in logic no
 r foundations of mathematics\, in particular no prior knowledge of these t
 opics is needed.\n
LOCATION:https://stable.researchseminars.org/talk/ProofUSACH/1/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Riccardo Brasca (Université Paris-Cité)
DTSTART:20221027T180000Z
DTEND:20221027T193000Z
DTSTAMP:20260404T094503Z
UID:ProofUSACH/2
DESCRIPTION:Title: <a href="https://stable.researchseminars.org/talk/Proof
 USACH/2/">The Lean proof assistant</a>\nby Riccardo Brasca (Université Pa
 ris-Cité) as part of An introduction to proof assistants: a mini course a
 bout mathematical formalization\n\n\nAbstract\nThere are several software 
 that can be used to formalize mathematics\, called <i>proof assistants</i>
 . One of the most used today by mathematician is <i>Lean</i>: it has a hug
 e library of already formalized mathematics\, <i>Mathlib</i>\, that allows
  to treat serious mathematics almost as we do ``on the blackboard''. I wil
 l explain 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 they will be solved in the (hopefully near) future.\n
LOCATION:https://stable.researchseminars.org/talk/ProofUSACH/2/
END:VEVENT
BEGIN:VEVENT
SUMMARY:Riccardo Brasca (Université Paris-Cité)
DTSTART:20221102T143000Z
DTEND:20221102T160000Z
DTSTAMP:20260404T094503Z
UID:ProofUSACH/3
DESCRIPTION:Title: <a href="https://stable.researchseminars.org/talk/Proof
 USACH/3/">Examples and exercises about formalization mathematics in Lean</
 a>\nby Riccardo Brasca (Université Paris-Cité) as part of An introductio
 n to proof assistants: a mini course about mathematical formalization\n\n\
 nAbstract\nI will give several examples of formalization of small results 
 in Lean\, both starting from scratch and using Mathlib. The goal of this f
 inal day is to let the audience ''play'' with Lean in practice\, proving r
 eal world theorems.\n
LOCATION:https://stable.researchseminars.org/talk/ProofUSACH/3/
END:VEVENT
END:VCALENDAR