BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CERN//INDICO//EN
BEGIN:VEVENT
SUMMARY:Informal introduction to formal proofs in Lean 4
DTSTART:20261020T090000Z
DTEND:20261020T100000Z
DTSTAMP:20261029T024800Z
UID:indico-event-17564@indico.math.cnrs.fr
DESCRIPTION:Speakers: Mykola Iorgov (Bogolyubov Institute for Theoretical 
 Physics\, Kyiv\, Ukraine)\n\nI will give an introduction to Lean 4\, a mod
 ern functional programming language with a powerful type system. One of i
 ts key features is the ability to state mathematical claims and write the
 ir proofs in Lean itself. This approach is based on the idea of “progra
 ms as proofs” (the Curry–Howard correspondence): a mathematical state
 ment is treated as a type\, and its proof as an element of that type. So w
 hen Lean checks a program\, it is in effect verifying the correctness of 
 the corresponding mathematical proof. If the code is accepted by Lean's k
 ernel\, we obtain a formally verified mathematical proof. This approach i
 s especially significant in modern research involving large language mode
 ls. LLMs can generate mathematical proofs\, and writing a proof in Lean m
 akes it possible to formally verify that it is correct.\n\nhttps://indico
 .math.cnrs.fr/event/17564/
LOCATION:Salle 1180\, bâtiment E2 (Salle des séminaires )
URL:https://indico.math.cnrs.fr/event/17564/
END:VEVENT
END:VCALENDAR