BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Assia Mahboubi (Inria\, France & VU Amsterdam\, Netherlands) DTSTART:20201020T140000Z DTEND:20201020T150000Z DTSTAMP:20260423T024647Z UID:CRM-CAMP/20 DESCRIPTION:Title: Formally verified computer-assisted mathematical proofs\nby Assia Ma hboubi (Inria\, France & VU Amsterdam\, Netherlands) as part of CRM CAMP ( Computer-Assisted Mathematical Proofs) in Nonlinear Analysis\n\n\nAbstract \nProof assistants are pieces of software designed for defining formally  mathematical objects\, statement and proofs. In particular\, such a forma lization reduces the verification of proofs to a purely mechanical well-f ormedness check. Since the early 70s\, proof\nassistants have been extensi vely used for applications in program verification\, notably for security -related issues. They have also been used to verify landmark results in m athematics\, including theorems with a computational proof\, like the Fou r Colour Theorem (Appel and Haken\, 1977) or Hales and Ferguson's proof o f the Kepler conjecture (2005). This talk will discuss what are formalize d mathematics and formal proofs\, and sketch the architecture of modern p roof assistants. It will also showcase a few applications in formally ve rified rigorous computation.\n LOCATION:https://researchseminars.org/talk/CRM-CAMP/20/ END:VEVENT END:VCALENDAR