BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Riccardo Brasca (Université Paris-Cité)
DTSTART:20221102T143000Z
DTEND:20221102T160000Z
DTSTAMP:20260412T203728Z
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