BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Filippo Nuccio (Université Jean Monnet Saint-Étienne)
DTSTART:20211022T143000Z
DTEND:20211022T153000Z
DTSTAMP:20260423T021420Z
UID:ANTULaval/4
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/ANTULaval/4/
 ">Explaining the finiteness of the class group of a number field to a comp
 uter</a>\nby Filippo Nuccio (Université Jean Monnet Saint-Étienne) as pa
 rt of Algebra and Number Theory Seminars at Université Laval\n\n\nAbstrac
 t\nA proof-assistant is a computer program that can digest a mathematical 
 proof\, implemented as a chain of statements. If all statements follow log
 ically from previously proven ones\, then the assistant is happy\, and cer
 tifies the correctness of the proof\; if it is doubtful about a certain po
 int\, it will not let you continue until it gets convinced. Among other pr
 oof assistants\, Lean3 is getting popular among some "classical" mathemati
 cians\, who are formalising well-known proofs in order to shape a larger a
 nd larger mathematical library upon which subsequent work can rely. In thi
 s talk\, I will show how to discuss with Lean3\, I will show some examples
  and I will report on a recent work\, joint with A. Baanen\, S. Daamen and
  Ashvni N.\, where we formalised the finiteness of the class group of a nu
 mber field in Lean3.\n
LOCATION:https://researchseminars.org/talk/ANTULaval/4/
END:VEVENT
END:VCALENDAR