BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CERN//INDICO//EN
BEGIN:VEVENT
SUMMARY:Formalizing Number Theory in Lean [MPIM]
DTSTART:20250130T140000Z
DTEND:20250130T150000Z
DTSTAMP:20260514T100900Z
UID:indico-event-227@math-events.uni-bonn.de
DESCRIPTION:Speakers: María Inés de Frutos Fernández (Universität Bonn
 )\n\nMPI-Oberseminar\nMathematical formalization is the process of digitiz
 ing mathematical definitions and results using a "proof assistant"\, a com
 puter program capable of checking logical statements against a set of infe
 rence rules and some basic axioms. In recent years\, the community of math
 ematicians working on formalization has grown rapidly and has reached mile
 stones that demonstrate the ability to formalize results at the frontier o
 f knowledge. Proof assistants have applications to mathematical research\,
  teaching\, and communication.\nAfter a brief introduction to formalizatio
 n\, I will present several of my  formalization results in the Lean inter
 active proof assistant\, from sub-areas of number theory including class f
 ield theory\, p-adic Hodge theory\, and the theory of Drinfeld modules.\n\
 nhttps://math-events.uni-bonn.de/event/227/
LOCATION:MPIM\, Vivatsgasse\,  7 - Lecture Hall (Max Planck Institute for 
 Mathematics)
URL:https://math-events.uni-bonn.de/event/227/
END:VEVENT
END:VCALENDAR